From 35b88f83d5ef0e1c1581466d03c156587748989f Mon Sep 17 00:00:00 2001
From: glondu
Date: Fri, 30 Jan 2009 22:04:25 +0000
Subject: More portable way to pipe stderr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11874 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.doc b/Makefile.doc
index 5a02817e5b..5e955a2614 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -67,7 +67,7 @@ HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file"
 SHOWMAKEINDEXERROR=egrep "^!! Input index error|^** Input style error|^   --"
 
 # Empty subsection levels in faq are on purpose
-HEVEAFAQFILTER=|& grep -v "^Warning: List with no item"
+HEVEAFAQFILTER=2>&1 | grep -v "^Warning: List with no item"
 
 ######################################################################
 # Common
-- 
cgit v1.2.3