diff options
| author | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-18 13:07:54 +0200 |
| commit | 4ee0cedff7726a56ebd53125995a7ae131660b4a (patch) | |
| tree | f5049f849a27b518f5c27298058df620a0ca38b3 /Makefile.build | |
| parent | aa926429727f1f6b5ef07c8912f2618d53f6d155 (diff) | |
Rename VM-related kernel/cfoo files to kernel/vmfoo
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 7806dce79c..4fb4b12be2 100644 --- a/Makefile.build +++ b/Makefile.build @@ -367,7 +367,7 @@ kernel/byterun/coq_jumptbl.h: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< jump > $@ -kernel/copcodes.ml: kernel/genOpcodeFiles.exe +kernel/vmopcodes.ml: kernel/genOpcodeFiles.exe $(SHOW)'WRITE $@' $(HIDE)$< copml > $@ |