aboutsummaryrefslogtreecommitdiffstats
path: root/src/VericertClflags.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-10-18 17:05:46 +0100
committerYann Herklotz <git@yannherklotz.com>2021-10-18 17:05:46 +0100
commitfbfa988072ce2eba808b9a6631af5f8e86cd9df0 (patch)
tree5146e558d5c9c6e9a399225eed0784b8dc12558f /src/VericertClflags.ml
parent603768a49eac2005729dd03e723ff6c5a6b292f7 (diff)
parentfe06668f0de56635efe55310d7a64289a37c1d90 (diff)
downloadvericert-dev/michalis.tar.gz
vericert-dev/michalis.zip
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'src/VericertClflags.ml')
-rw-r--r--src/VericertClflags.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml
index 977ca00..ab3c949 100644
--- a/src/VericertClflags.ml
+++ b/src/VericertClflags.ml
@@ -5,6 +5,7 @@ let option_debug_hls = ref false
let option_initial = ref false
let option_dhtl = ref false
let option_drtlblock = ref false
+let option_drtlpar = ref false
let option_hls_schedule = ref false
let option_fif_conv = ref false
let option_fram = ref true