diff options
Diffstat (limited to 'kernel/byterun/dune')
| -rw-r--r-- | kernel/byterun/dune | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/byterun/dune b/kernel/byterun/dune index c3c44670be..20bdf28e54 100644 --- a/kernel/byterun/dune +++ b/kernel/byterun/dune @@ -5,6 +5,9 @@ (c_names coq_fix_code coq_memory coq_values coq_interp)) (rule + (targets coq_instruct.h) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe enum)))) + +(rule (targets coq_jumptbl.h) - (deps (:h-file coq_instruct.h) make_jumptbl.sh) - (action (bash "./make_jumptbl.sh %{h-file} %{targets}"))) + (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump)))) |