aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Bernhard Schommer <bernhardschommer@gmail.com>2018-01-11 15:36:34 +0100
committerGravatar Bernhard Schommer <bernhardschommer@gmail.com>2018-01-11 15:36:34 +0100
commit8de997434f5002728840123dab3aa3e899d1d3f2 (patch)
tree1303972c3b822ba5493fb19e4bd5a1c1dd1e82e1 /tools
parentd439c01190f45de5ac493b8f55d361503e83ad03 (diff)
Added newline at the end of usage of coqdep.
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index fd4be08b1..2433cb1d0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -455,7 +455,7 @@ let usage () =
eprintf " -coqlib dir : set the coq standard library directory\n";
eprintf " -suffix s : \n";
eprintf " -slash : deprecated, no effect\n";
- eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed";
+ eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed\n";
exit 1
let split_period = Str.split (Str.regexp (Str.quote "."))