diff options
Diffstat (limited to 'xserver/doc/filter-xmlto.sh')
-rw-r--r-- | xserver/doc/filter-xmlto.sh | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/xserver/doc/filter-xmlto.sh b/xserver/doc/filter-xmlto.sh new file mode 100644 index 000000000..3596ed13a --- /dev/null +++ b/xserver/doc/filter-xmlto.sh @@ -0,0 +1,21 @@ +#!/bin/sh +# +# Run the xmlto command, filtering its output to +# reduce the amount of useless warnings in the build log. +# +# Exit with the status of the xmlto process, not the status of the +# output filtering commands +# +# This is a bit twisty, but avoids any temp files by using pipes for +# everything. It routes the command output through file +# descriptor 4 while sending the (numeric) exit status through +# standard output. +# +(((("$@" 2>&1; echo $? >&3) | + grep -v overflows | + grep -v 'Making' | + grep -v 'hyphenation' | + grep -v 'Font.*not found' | + grep -v '/tmp/xml' | + grep -v Rendered >&4) 3>&1) | + (read status; exit $status)) 4>&1 |