Minor bugfix after merge