diff options
| author | glondu | 2010-07-02 12:54:57 +0000 |
|---|---|---|
| committer | glondu | 2010-07-02 12:54:57 +0000 |
| commit | dacb4b76afe554f1a1e17d981bc98d9fc3a8e807 (patch) | |
| tree | 0c6de9a4f3a7338f32f70520d9647e6f3a356497 /Makefile.build | |
| parent | 2de4563cb6192e638df4172c725ec8814e6eb112 (diff) | |
Remove dependency to Unix from module Profile
Looking at the source code of Sys.time reveals that it is exactly what
is computed by Profile.get_time. This can also be tested by evaluating:
Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);;
in an OCaml toplevel with Unix.
This allows to put Profile in grammar.cma without the dependency to
unix.cma while preprocessing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.build b/Makefile.build index 6af048572f..adba237537 100644 --- a/Makefile.build +++ b/Makefile.build @@ -655,7 +655,7 @@ dev/printers.cma: | dev/printers.mllib.d parsing/grammar.cma: | parsing/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) unix.cma $^ -impl" -impl test.ml4 -o test-grammar + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) $^ -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ @@ -801,7 +801,7 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)\ DEPS=$(CAMLP4DEPS); \ if ls $${DEPS} > /dev/null 2>&1; then \ - $(CAMLP4O) $(PR_O) -I $(CAMLLIB) unix.cma $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ + $(CAMLP4O) $(PR_O) -I $(CAMLLIB) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ else echo $< : Dependency $${DEPS} not ready yet; false; fi %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) |