Commit 803e6561 authored by Ralf Jung's avatar Ralf Jung

remove no-longer-needed Makefile hackery

parent 721c4e26
Pipeline #12738 passed with stage
in 15 minutes and 44 seconds