From eb479438328a473ff1cf5fe010ed714194dbf28f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 00:50:19 +0200
Subject: [pp] Fix newline issues.

This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where
we got a few cases wrong wrt to newline endings.

Thanks to @herbelin for pointing it out.

This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
---
 proofs/refiner.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ebd30820be..ea8543b02f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -221,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   Feedback.msg_notice
     (str (emacs_str "<infoH>")
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")) ++ fnl());
+      ++  (str (emacs_str "</infoH>")));
   tclIDTAC goal;;
 
 
-- 
cgit v1.2.3