diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-18 16:56:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-18 16:56:17 +0000 |
| commit | b28e9663968e55b0edd79af09581f8fe31337821 (patch) | |
| tree | 7cae03a2dd953e1c74c3a83fae8c882847851337 /Makefile.build | |
| parent | 95e8234b7a3e3850710a18d26f6dd561497e25d0 (diff) | |
coqc and coqmktop migrated in tools/, get rid of scripts/ subdir
No need to place these binaries apart, and anyway they aren't
(shell) scripts since ages.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 6c2435702..b42432d48 100644 --- a/Makefile.build +++ b/Makefile.build @@ -254,7 +254,7 @@ $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, $(OSDEPLIBS), $(SYSMOD)) -scripts/tolink.ml: Makefile.build Makefile.common +tools/tolink.ml: Makefile.build Makefile.common $(SHOW)"ECHO... >" $@ $(HIDE)echo "let copts = \"-cclib -lcoqrun\"" > $@ $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@ |