aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-14 11:20:34 +0200
committerHugo Herbelin2019-05-14 11:37:50 +0200
commit00d05ff204108622d1f944d748103a98c0d6d088 (patch)
treee1ad069b029d80f0d696c29ed1558ad998988748
parentdf98a88a1e35213e994ec583f6ad4e0d3ccac868 (diff)
Adding missing newline in coqc usage.
-rw-r--r--toplevel/usage.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 3d15cb0274..04b23f587f 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -107,7 +107,7 @@ coqtop specific options:\
exit 1
let print_usage_coqc () =
- print_usage_common stderr "Usage: coqc <options> <Coq options> file...";
+ print_usage_common stderr "Usage: coqc <options> <Coq options> file...\n\n";
output_string stderr "\n\
coqc specific options:\
\n\