aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 10:36:58 +0000
committerGravatar regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 10:36:58 +0000
commit98749c9a507fb4a5bfec049ec7828eb357766884 (patch)
tree21cf7503e76a935eb587e23a008c1419e55bef32 /tools
parent9a2f43eca179436f0581751b93c989fd30a5c13c (diff)
* tools/Coq_makefile
Export $(COQMKTOP) in generated Makefiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16028 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index bc90caafe..cbc6df2ff 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -399,6 +399,7 @@ let variables is_install opt (args,defs) =
print "GALLINA?=$(COQBIN)gallina\n";
print "COQDOC?=$(COQBIN)coqdoc\n";
print "COQCHK?=$(COQBIN)coqchk\n\n";
+ print "COQMKTOP?=$(COQBIN)coqmktop\n\n";
end;
(* Caml executables and relative variables *)
if !some_ml4file || !some_mlfile || !some_mlifile then begin