git.annexia.org
/
goals.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
ce72c65
)
Change -V to -v for compat with make.
author
Richard W.M. Jones
<rjones@redhat.com>
Mon, 30 Dec 2019 21:41:17 +0000
(21:41 +0000)
committer
Richard W.M. Jones
<rjones@redhat.com>
Mon, 30 Dec 2019 21:59:21 +0000
(21:59 +0000)
src/cmdline.ml
patch
|
blob
|
history
diff --git
a/src/cmdline.ml
b/src/cmdline.ml
index
53ab0f9
..
b7063af
100644
(file)
--- a/
src/cmdline.ml
+++ b/
src/cmdline.ml
@@
-72,7
+72,7
@@
let input_file, directory, includes, use_prelude, anon_vars, targets =
"dir Add include directory";
"--no-prelude",Arg.Clear use_prelude,
" Do not automatically use prelude.gl from stdlib";
- "-
V
", Arg.Unit print_version,
+ "-
v
", Arg.Unit print_version,
" Print version and exit";
"--version", Arg.Unit print_version,
" Print version and exit";