From db278921c54201a01543953cc0986fc0fb126615 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 5 Oct 2020 22:21:04 +0200
Subject: Dropping the misleading int argument of Pp.h.

An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.

We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
---
 plugins/extraction/scheme.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index ee50476b10..f671860bd5 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -28,7 +28,7 @@ let keywords =
       "error"; "delay"; "force"; "_"; "__"]
     Id.Set.empty
 
-let pp_comment s = str";; "++h 0 s++fnl ()
+let pp_comment s = str ";; " ++ h s ++ fnl ()
 
 let pp_header_comment = function
   | None -> mt ()
-- 
cgit v1.2.3