From 8541a43c053d659196992f4e990ec317cd199af8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 21 Feb 2019 16:45:12 +0000
Subject: [Kernel] Simpler generation of opcode files

Files kernel/copcodes.ml, kernel/byterun/coq_instruct.h, and
kernel/byterun/coq_jumptbl.h are generated by a simple OCaml program
rather than a pipeline of sed and awk text processing.
---
 kernel/byterun/dune | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'kernel/byterun/dune')

diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index c3c44670be..20bdf28e54 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -4,7 +4,10 @@
  (public_name coq.vm)
  (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))))
-- 
cgit v1.2.3