diff options
| author | Emilio Jesus Gallego Arias | 2019-03-01 19:31:50 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-01 19:31:50 +0100 |
| commit | 1e03d1e666e74b95b9936bfdd6f04d54c607c37f (patch) | |
| tree | 01fa5d89b158dd019cca34b4b5aab2b7e46a0a6d /kernel/byterun/dune | |
| parent | 74016bb28f1176aa9dce5f897f434729c2c99c93 (diff) | |
| parent | 8541a43c053d659196992f4e990ec317cd199af8 (diff) | |
Merge PR #9624: [Kernel] Simpler generation of opcode files
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: rgrinberg
Ack-by: vbgl
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)))) |