aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/goptions.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/goptions.ml')
-rw-r--r--library/goptions.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/library/goptions.ml b/library/goptions.ml
index 858ebbfc8..550ded685 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -105,10 +105,10 @@ module MakeTable =
let print_table table_name printer table =
pp (str table_name ++
(hov 0
- (if MySet.is_empty table then str "None" ++ fnl ()
+ (if MySet.is_empty table then str " None" ++ fnl ()
else MySet.fold
- (fun a b -> printer a ++ spc () ++ b)
- table (mt ()) ++ fnl ())))
+ (fun a b -> spc () ++ printer a ++ b)
+ table (mt ()) ++ str "." ++ fnl ())))
class table_of_A () =
object