summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJonathan Protzenko2022-01-04 12:47:27 -0800
committerJonathan Protzenko2022-01-04 12:47:27 -0800
commit9872966d3c7a97ce8cd9ef16ab934ffa09c23e13 (patch)
tree868cbb777ae8e07b63123e90d2cdacc8371f1d5f
parentcf873d92162cad0cabaa580e18f7412df605cc85 (diff)
one remark
Diffstat (limited to '')
-rw-r--r--src/main.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/main.ml b/src/main.ml
index 4616aadf..546f09a8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -10,7 +10,8 @@ type test = Test [@@deriving show]
let _ = show_test Test
(* This is necessary to have a backtrace when raising exceptions - for some
- * reason, the -g option doesn't work *)
+ * reason, the -g option doesn't work.
+ * JP: are you running with OCAMLRUNPARAM=b=1? *)
let () = Printexc.record_backtrace true
let usage = Printf.sprintf {|Aenaes: verification of Rust programs by translation