aboutsummaryrefslogtreecommitdiffstats
path: root/common/PrintAST.ml
diff options
context:
space:
mode:
Diffstat (limited to 'common/PrintAST.ml')
-rw-r--r--common/PrintAST.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index e477957a..baddb722 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -90,3 +90,7 @@ let rec print_builtin_res px oc = function
fprintf oc "splitlong(%a, %a)"
(print_builtin_res px) hi (print_builtin_res px) lo
+let print_trapping_mode oc = function
+ | TRAP -> ()
+ | NOTRAP -> output_string oc " [notrap]"
+