2019-05-09 11:23:50 +00:00
|
|
|
#!/bin/sh
|
|
|
|
set -e
|
|
|
|
|
|
|
|
if [ -z "$1" ]; then
|
|
|
|
echo "Use: $0 page-name (with no section suffix)"
|
|
|
|
exit 1
|
|
|
|
fi
|
|
|
|
|
|
|
|
target="man/$1.html"
|
|
|
|
ninja -C "@BUILD_ROOT@" "$target"
|
|
|
|
set -x
|
2019-06-04 15:33:59 +00:00
|
|
|
exec xdg-open "@BUILD_ROOT@/$target"
|