Skip to content

Instantly share code, notes, and snippets.

@moratorium08
Created December 5, 2019 03:55
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save moratorium08/9651694a281bf3dc7173bee29da65438 to your computer and use it in GitHub Desktop.
Save moratorium08/9651694a281bf3dc7173bee29da65438 to your computer and use it in GitHub Desktop.
diff --git a/Makefile b/Makefile
index 805ad11..ca019d0 100644
--- a/Makefile
+++ b/Makefile
@@ -39,13 +39,13 @@ revision.ml: $(FPAT_LIB) Makefile Makefile.config
@echo make revision.ml
@rm -f $@
ifdef GIT
- @echo -n 'let mochi = Some ("' >> $@
- @if [ $$(${GIT} diff | wc -w) != 0 ]; then echo -n _ >> $@; fi
- @echo -n `$(GIT) rev-parse --short HEAD` >> $@
- @echo -n '", "' >> $@
- @if [ $$(${GIT} diff | wc -w) != 0 ]; then echo -n "after " >> $@; fi
+ @/bin/echo -n 'let mochi = Some ("' >> $@
+ @if [ $$(${GIT} diff | wc -w) != 0 ]; then /bin/echo -n _ >> $@; fi
+ @/bin/echo -n `$(GIT) rev-parse --short HEAD` >> $@
+ @/bin/echo -n '", "' >> $@
+ @if [ $$(${GIT} diff | wc -w) != 0 ]; then /bin/echo -n "after " >> $@; fi
@$(GIT) log --date=iso --pretty=format:"%ad" -1 >> $@
- @echo '")' >> $@
+ @/bin/echo '")' >> $@
else
@echo "let mochi = None" >> $@
endif
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment