diff options
Diffstat (limited to 'Makefile.make')
| -rw-r--r-- | Makefile.make | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.make b/Makefile.make index 2f6781439c..aafa323b4f 100644 --- a/Makefile.make +++ b/Makefile.make @@ -109,7 +109,7 @@ GENGRAMMLFILES := $(GRAMMLFILES) gramlib/.pack/gramlib.ml # why is gramlib.ml no GENMLGFILES:= $(MLGFILES:.mlg=.ml) GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) $(GENGRAMMLFILES) ide/coqide/coqide_os_specific.ml kernel/vmopcodes.ml kernel/uint63.ml kernel/float64.ml GENMLIFILES:=$(GRAMMLIFILES) -GENHFILES:=kernel/byterun/coq_instruct.h kernel/byterun/coq_jumptbl.h +GENHFILES:=$(addprefix kernel/byterun/, coq_instruct.h coq_jumptbl.h coq_arity.h) GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) kernel/genOpcodeFiles.exe COQ_EXPORTED += GRAMFILES GRAMMLFILES GRAMMLIFILES GENMLFILES GENHFILES GENFILES |