1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
|
#!/bin/sh
# makeinfo wrapper that post-processes HTML output to replace _002d with -,
# only on lines containing "option", corresponding to our @optAnchor macro.
# Note texi uses "-" in anchors for spaces, hence why it escapes - with _002d.
@MAKEINFO@ "$@" || exit
process_html()
{
sed_anchor_cleanup=\
'/id=.*_002doption/{ s/id="\([^"]*\)_002doption/id="\1/g; s/_002d/-/g; }'
sed -e "$sed_anchor_cleanup" "$1" > "$1.t" &&
mv "$1.t" "$1"
}
case " $* " in
*" --html"*)
# Find the output file/directory
output=""
next_is_output=false
for arg in "$@"; do
if [ "$next_is_output" = true ]; then
output="$arg"
break
fi
case "$arg" in
-o) next_is_output=true ;;
--output=*) output="${arg#--output=}" ;;
esac
done
# Process the output file/directory
if test -n "$output"; then
test -f "$output" && NAMES='*' || NAMES='*.html'
find "$output" -name "$NAMES" -type f |
# dash doesn't support read -d '' yet.
while IFS= read -r htmlfile; do process_html "$htmlfile"; done
fi
;;
esac
|
