diff options
| -rw-r--r-- | Makefile.build | 2 | ||||
| -rw-r--r-- | configure.ml | 8 |
2 files changed, 9 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index c71c719a6c..face3e34d6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -372,7 +372,7 @@ install-ide-info: md5chk: $(SHOW)'MD5SUM cic.mli' - $(HIDE)if grep -q `md5sum checker/cic.mli` checker/values.ml; \ + $(HIDE)if grep -q `$(MD5SUM) checker/cic.mli` checker/values.ml; \ then true; else echo "Error: outdated checker/values.ml"; false; fi VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m diff --git a/configure.ml b/configure.ml index 3b5daee3c0..6e0b610fc6 100644 --- a/configure.ml +++ b/configure.ml @@ -758,6 +758,12 @@ let strip = if !Prefs.profile || !Prefs.debug then "true" else "strip" +(** * md5sum command *) + +let md5sum = + if arch = "Darwin" then "md5 -q" else "md5sum" + + (** * Documentation : do we have latex, hevea, ... *) let check_doc () = @@ -1097,6 +1103,8 @@ let write_makefile f = pr "# Unix systems and profiling: true\n"; pr "# Unix systems and no profiling: strip\n"; pr "STRIP=%s\n\n" strip; + pr "#the command md5sum\n"; + pr "MD5SUM=%s\n\n" md5sum; pr "# LablGTK\n"; pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes; pr "# CoqIde (no/byte/opt)\n"; |