aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-18 16:56:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-18 16:56:17 +0000
commitb28e9663968e55b0edd79af09581f8fe31337821 (patch)
tree7cae03a2dd953e1c74c3a83fae8c882847851337 /Makefile
parent95e8234b7a3e3850710a18d26f6dd561497e25d0 (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')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 9e1742a56..1d235d5b2 100644
--- a/Makefile
+++ b/Makefile
@@ -78,7 +78,7 @@ EXISTINGMLI := $(call find, '*.mli')
GENML4FILES:= $(ML4FILES:.ml4=.ml)
GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
- scripts/tolink.ml kernel/copcodes.ml
+ tools/tolink.ml kernel/copcodes.ml
GENMLIFILES:=$(YACCFILES:.mly=.mli)
GENPLUGINSMOD:=$(filter plugins/%,$(MLLIBFILES:%.mllib=%_mod.ml))
export GENHFILES:=kernel/byterun/coq_jumptbl.h