From 8f9727e1163352a3f1a01ee3d807f74f7f8d4640 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sun, 19 Sep 2010 10:22:18 +0000
Subject: Hopefully a fix for #2176 (redirection not understood with some
 shells)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13437 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/tools/show_latex_messages | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/show_latex_messages b/doc/tools/show_latex_messages
index 88044410a..8f1470ec1 100755
--- a/doc/tools/show_latex_messages
+++ b/doc/tools/show_latex_messages
@@ -1,8 +1,8 @@
 #!/bin/sh
 
 if [ "$1" = "-no-overfull" ]; then
-  ../tools/latex_filter `wc -l < $2` no < $2
+  cat $2 | ../tools/latex_filter `cat $2 | wc -l` no
 else
-  ../tools/latex_filter `wc -l < $1` yes < $1
+  cat $1 | ../tools/latex_filter `cat $1 | wc -l` yes
 fi
 
-- 
cgit v1.2.3