aboutsummaryrefslogtreecommitdiffstats
path: root/backend/JsonAST.ml
diff options
context:
space:
mode:
Diffstat (limited to 'backend/JsonAST.ml')
-rw-r--r--backend/JsonAST.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index 3469bdc6..4e57106f 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -123,15 +123,15 @@ let pp_mnemonics pp mnemonic_names =
let new_line pp () = pp_print_string pp "\n" in
pp_print_list ~pp_sep:new_line pp_print_string pp mnemonic_names
-let jdump_magic_number = "CompCertJDUMP" ^ Version.version
+let jdump_magic_number = "CompCertJDUMPRelease: " ^ Version.version
let pp_ast pp pp_inst ast sourcename =
let get_args () =
let buf = Buffer.create 100 in
Buffer.add_string buf Sys.executable_name;
- for i = 1 to (Array.length !Commandline.argv - 1) do
+ for i = 1 to (Array.length Commandline.argv - 1) do
Buffer.add_string buf " ";
- Buffer.add_string buf (Responsefile.gnu_quote !Commandline.argv.(i));
+ Buffer.add_string buf (Responsefile.gnu_quote Commandline.argv.(i));
done;
Buffer.contents buf in
let dump_compile_info pp () =