diff options
| author | letouzey | 2013-04-18 16:56:17 +0000 |
|---|---|---|
| committer | letouzey | 2013-04-18 16:56:17 +0000 |
| commit | b28e9663968e55b0edd79af09581f8fe31337821 (patch) | |
| tree | 7cae03a2dd953e1c74c3a83fae8c882847851337 /Makefile.common | |
| 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.common')
| -rw-r--r-- | Makefile.common | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index 63834dcb04..1934fd4938 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,7 +72,7 @@ PLUGINS:=\ SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc scripts \ + tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) IDESRCDIRS:=\ @@ -224,9 +224,9 @@ IDEMOD:=$(shell cat ide/ide.mllib) COQENVCMO:=lib/clib.cma lib/loc.cmo lib/errors.cmo -COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo +COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo -COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo +COQCCMO:=$(COQENVCMO) toplevel/usage.cmo tools/coqc.cmo ## Misc |