aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/Clightgen.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index 637454f0..5e27370e 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -91,7 +91,7 @@ let process_i_file sourcename =
compile_c_file sourcename sourcename ofile
let usage_string =
- version_string tool_name^
+ version_string tool_name ^
{|Usage: clightgen [options] <source files>
Recognized source files:
.c C source file
@@ -99,7 +99,7 @@ Recognized source files:
Processing options:
-normalize Normalize the generated Clight code w.r.t. loads in expressions
-canonical-idents Use canonical numbers to represent identifiers (default)
- -short-idents Use canonical numbers to represent identifiers
+ -short-idents Use small, non-canonical numbers to represent identifiers
-E Preprocess only, send result to standard output
-o <file> Generate output in <file>
|} ^