Commit e0c66e81 authored by Ralf Jung's avatar Ralf Jung

remove no-longer-needed Makefile hackery

parent ebdaa70f
Pipeline #12745 failed with stage
in 17 minutes and 19 seconds