aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pputils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/pputils.ml')
-rw-r--r--printing/pputils.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 4ae5035a2..d1ba1a4a1 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -15,14 +15,15 @@ open Locus
open Genredexpr
let pr_located pr (loc, x) =
- if !Flags.beautify && not (Loc.is_ghost loc) then
+ match loc with
+ | Some loc when !Flags.beautify ->
let (b, e) = Loc.unloc loc in
(* Side-effect: order matters *)
let before = Pp.comment (CLexer.extract_comments b) in
let x = pr x in
let after = Pp.comment (CLexer.extract_comments e) in
before ++ x ++ after
- else pr x
+ | _ -> pr x
let pr_or_var pr = function
| ArgArg x -> pr x