diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index b307bde5df..d619fd3c85 100644 --- a/Makefile.build +++ b/Makefile.build @@ -367,6 +367,10 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< jump > $@ +kernel/byterun/coq_arity.h: kernel/genOpcodeFiles.exe + $(SHOW)'WRITE $@' + $(HIDE)$< arity > $@ + kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< copml > $@ |