aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-01 11:08:01 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2020-06-01 11:08:01 +0200
commit08491de0566dbd8cfe7a9cd4ca129a5a05caf196 (patch)
tree1c58a5c6a3effa02ad2c6810f6ab222132c755f0 /exportclight
parent18859319b1daee0abb32bbc4e89ec5865a6fe082 (diff)
downloadcompcert-kvx-08491de0566dbd8cfe7a9cd4ca129a5a05caf196.tar.gz
compcert-kvx-08491de0566dbd8cfe7a9cd4ca129a5a05caf196.zip
clightgen: fix usage message
Closes: #358
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>
|} ^