diff --git a/goaljobs.ml b/goaljobs.ml index 0d6f56b13c38240e99aa18d8d95e9ce56e1e5740..d62a3d95703e286b10f6da7283eedc528a886e44 100644 --- 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 [