aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-10-31 15:29:57 +0100
committerGaëtan Gilbert2018-11-02 13:48:16 +0100
commit00a8604d89f47c903fc5283eebdda67c87468699 (patch)
treef67746d0dc474fb6d7d239c269efd43f44678376 /Makefile
parent9b0a4b002e324d523b01e17fba7ba631a651f6b0 (diff)
Select OS specific coqide code with cp.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index f2dc6d7750..b9d8bf34e3 100644
--- a/Makefile
+++ b/Makefile
@@ -96,7 +96,7 @@ EXISTINGMLI := $(call find, '*.mli')
GENML4FILES:= $(ML4FILES:.ml4=.ml)
GENMLGFILES:= $(MLGFILES:.mlg=.ml)
-export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml
+export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml
export GENHFILES:=kernel/byterun/coq_jumptbl.h
export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES)