From 11789ba0f936f6d4095cd1b761817557cf69ba3f Mon Sep 17 00:00:00 2001
From: Ludovic Court`es
Date: Mon, 3 Sep 2007 17:23:04 +0000
Subject: skribilo: Flush the output port before exiting.

* src/guile/skribilo.scm (skribilo): Flush `(*skribilo-output-port*)'
  before exiting.

git-archimport-id: lcourtes@laas.fr--2006-libre/skribilo--devo--1.2--patch-105
---
 src/guile/skribilo.scm | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/guile/skribilo.scm b/src/guile/skribilo.scm
index 106fc71..8559de3 100644
--- a/src/guile/skribilo.scm
+++ b/src/guile/skribilo.scm
@@ -464,10 +464,12 @@ Processes a Skribilo/Skribe source file and produces its output.
 
 	    (setvbuf (*skribilo-output-port*) _IOFBF 16384)
 
-	    ;;	(start-stack 7
 	    (if source-file
 		(with-input-from-file source-file doskribe)
-		(doskribe))))))))
+		(doskribe))
+
+            ;; Make sure the output port is flushed before we leave.
+            (force-output (*skribilo-output-port*))))))))
 
 
 (define main skribilo)
-- 
cgit v1.2.3