Delete file which became obsolete in previous commit
Delete file which became obsolete in previous commit

This could have been deleted in the previous commit already, but git
wrongly detected it as a rename, so it is done separately for clarity.

See commit 793fd0f3b527fdc6ad2dbb21a6b64b626c1050e2

danielschenk/mlc2,danielschenk/mlc2,danielschenk/mlc2