aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--parsing/printer.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 63accefd1..bfb571b23 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -474,6 +474,9 @@ let pr_prim_rule = function
(str (if withdep then "dependent " else "") ++
str"move " ++ pr_id id1 ++ pr_move_location pr_id id2)
+ | Order ord ->
+ (str"order " ++ prlist_with_sep pr_spc pr_id ord)
+
| Rename (id1,id2) ->
(str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2)