diff options
| -rw-r--r-- | Makefile.build | 22 | ||||
| -rw-r--r-- | Makefile.common | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 9 |
3 files changed, 19 insertions, 14 deletions
diff --git a/Makefile.build b/Makefile.build index 97bab95df5..6312feff70 100644 --- a/Makefile.build +++ b/Makefile.build @@ -796,15 +796,17 @@ ifeq ($(CHECKEDOUT),git) fi endif $(HIDE)set -e; \ - if test -e revision; then \ + if test -e revision.new; then \ + if test -e revision; then \ if test "`cat revision`" = "`cat revision.new`" ; then \ rm -f revision.new; \ else \ mv -f revision.new revision; \ fi; \ - else \ + else \ mv -f revision.new revision; \ - fi + fi \ + fi ########################################################################### # Default rules @@ -859,7 +861,7 @@ endif %.ml: %.mll $(SHOW)'OCAMLLEX $<' - $(HIDE)$(OCAMLLEX) $< + $(HIDE)$(OCAMLLEX) "$*.mll" -o $@ %.ml %.mli: %.mly $(SHOW)'OCAMLYACC $<' @@ -900,27 +902,27 @@ endif #Critical section: # Nobody (in a make -j) should touch the .ml file here. $(SHOW)'OCAMLDEP4 $<' - $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $*.ml \ + $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< -o $*.ml \ || ( RV=$$?; rm -f "$*.ml"; exit $${RV} ) - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $*.ml | sed '' > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(HIDE)echo "let keep_ocamldep_happy Do_not_compile_me = assert false" > $*.ml #End critical section checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@" + $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@" checker/%.mli.d: $(D_DEPEND_BEFORE_SRC) checker/%.mli $(D_DEPEND_AFTER_SRC) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) $< > "$@" + $(HIDE)$(OCAMLDEP) -slash $(LOCALCHKLIBS) "$<" | sed '' > "$@" %.ml.d: $(D_DEPEND_BEFORE_SRC) %.ml $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@" + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@" %.mli.d: $(D_DEPEND_BEFORE_SRC) %.mli $(D_DEPEND_AFTER_SRC) $(GENFILES) $(ML4FILES:.ml4=.ml) $(SHOW)'OCAMLDEP $<' - $(HIDE)$(OCAMLDEP) $(DEPFLAGS) $< > "$@" + $(HIDE)$(OCAMLDEP) $(DEPFLAGS) "$<" | sed '' > "$@" ## Veerry nasty hack to keep ocamldep happy %.ml: | %.ml4 diff --git a/Makefile.common b/Makefile.common index 42197c98d6..7719572f02 100644 --- a/Makefile.common +++ b/Makefile.common @@ -44,7 +44,7 @@ OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE) MINICOQ:=bin/minicoq$(EXE) -CSDPCERT:=bin/csdpcert +CSDPCERT:=bin/csdpcert$(EXE) ########################################################################### # tools diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d09a87dc6a..0c9b12bb4a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -131,9 +131,12 @@ let set_opt () = re_exec_version := "opt" let re_exec is_ide = let s = !re_exec_version in let is_native = (Mltop.get()) = Mltop.Native in - let prog = - try Unix.readlink "/proc/self/exe" - with Unix.Unix_error _ -> Sys.argv.(0) in + (* Unix.readlink is not implemented on Windows architectures :-( + let prog = + try Unix.readlink "/proc/self/exe" + with Unix.Unix_error _ -> Sys.argv.(0) in + *) + let prog = Sys.argv.(0) in if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let s = if s = "" then if is_native then "opt" else "byte" else s in |