summaryrefslogtreecommitdiff
blob: 7b4acf01768968707c8bd9560a3fc6a34a28d1b6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
--- Makefile.orig	2004-06-19 23:53:43.231742696 +0200
+++ Makefile	2004-06-19 23:54:39.977116088 +0200
@@ -346,7 +346,7 @@
 
 $(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
+	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
 
 $(COQTOP):
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -570,7 +570,7 @@
 
 $(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@
+	$(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
 
 $(COQIDE):
 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)