aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 6 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 27c51a5a4..2dcf8cca9 100644
--- a/Makefile
+++ b/Makefile
@@ -216,9 +216,11 @@ COQC=bin/coqc$(EXE)
COQTOPBYTE=bin/coqtop.byte$(EXE)
COQTOPOPT=bin/coqtop.opt$(EXE)
BESTCOQTOP=bin/coqtop.$(BEST)$(EXE)
+COQTOP=bin/coqtop$(EXE)
COQINTERFACE=bin/coq-interface$(EXE) bin/parser
-COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQINTERFACE)
+COQBINARIES= $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(BESTCOQTOP) $(COQTOP) \
+ $(COQINTERFACE)
world: $(COQBINARIES) states theories contrib tools
@@ -229,6 +231,9 @@ $(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX)
$(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
$(COQMKTOP) -top $(INCLUDES) $(CAMLDEBUG) -o $@
+$(COQTOP):
+ cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
+
# coqmktop
COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo