395e2128 ^
fa3d7edc ^
b856e7e1 ^
60e11efc ^
1
2 3 4 5 6 7
8
9 10 11 12 13 14
#!/bin/bash # # Compile mu if necessary before running it. # show make output only if something needs doing make -q || make >&2 || exit 1 ./mu_bin $FLAGS "$@" # Scenarios considered: # mu # mu --help # mu test # mu test file1.mu