Closed barockobamo closed 5 years ago
Ah, I hadn't tested using dash before. I'm happy with the first option.
As it seems that /bin/sh -> dash
is the default on debian, we should not use curly braces expansion.
Removed Makefiles wildcard in clean section in #34
This happen on many of my debian machines. The clean section of Makefile was not able to execute these kind of command : clean : rm -f *.{cmi, cmo} We found out that we should ever :