Commit 55e54fd34a05637a3eac2cf6503e62b689c172c1

Stefan Sperling 2020-01-28T14:03:16

remove a Makefile chunk which is obsolete since bb5b19e3