diff options
Diffstat (limited to 'mu')
-rwxr-xr-x | mu | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/mu b/mu new file mode 100755 index 00000000..cd4019c5 --- /dev/null +++ b/mu @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# +# Compile mu if necessary before running it. + +# show make output only if something needs doing +make -q || make >&2 || exit 1 + +./mu_bin "$@" |