aboutsummaryrefslogtreecommitdiff
path: root/src/CLI.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-18 18:10:17 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-01-23 18:52:31 -0500
commitb48a0a78c26ec34b84fe10cb8efb2bf54d8d7584 (patch)
tree69a6291d67b809a4895416fc1352d090d197d98d /src/CLI.v
parentcdd5ffb086eb647eabe640c81de9d8af7cd0a1dd (diff)
Mention the separator (spaces) of the list arg
Diffstat (limited to 'src/CLI.v')
-rw-r--r--src/CLI.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/CLI.v b/src/CLI.v
index 3975b0845..b4ed87604 100644
--- a/src/CLI.v
+++ b/src/CLI.v
@@ -144,7 +144,7 @@ Module ForExtraction.
Definition machine_wordsize_help
:= " machine_wordsize The machine bitwidth (e.g., 32 or 64)".
Definition function_to_synthesize_help (valid_names : string)
- := " function_to_synthesize A list of functions that should be synthesized. If no functions are given, all functions are synthesized."
+ := " function_to_synthesize A space-separated list of functions that should be synthesized. If no functions are given, all functions are synthesized."
++ String.NewLine ++
" Valid options are " ++ valid_names.