git.annexia.org
/
goaljobs.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
b9524a7
)
-l/--goals option should exit after listing goals.
author
Richard W.M. Jones
<rjones@redhat.com>
Tue, 17 Sep 2013 11:31:59 +0000
(12:31 +0100)
committer
Richard W.M. Jones
<rjones@redhat.com>
Tue, 17 Sep 2013 11:38:01 +0000
(12:38 +0100)
goaljobs.ml
patch
|
blob
|
history
diff --git
a/goaljobs.ml
b/goaljobs.ml
index
0d6f56b
..
d62a3d9
100644
(file)
--- a/
goaljobs.ml
+++ b/
goaljobs.ml
@@
-312,7
+312,8
@@
let init () =
let names = !published_goals in
let names = List.map fst names in
let names = List.sort compare names in
- List.iter print_endline names
+ List.iter print_endline names;
+ exit 0
in
let argspec = Arg.align [