Revert "Dummy Makefile.in for CIs"
This reverts commit c55de95ff1c4ea6313c2863037703a0e5f0d0f4f.
Probably this is not needed for CI anymore.
Revert "Dummy Makefile.in for CIs"
This reverts commit c55de95ff1c4ea6313c2863037703a0e5f0d0f4f.
Probably this is not needed for CI anymore.