1 files changed, 16 insertions, 0 deletions
diff --git a/man/man.in b/man/man.in
new file mode 100755
index 0000000000..75680b860c
--- /dev/null
+++ b/man/man.in
@@ -0,0 +1,16 @@
+#!/bin/sh
+set -e
+
+if [ -z "$1" ]; then
+    echo "Use: $0 page-name (with no section suffix)"
+    exit 1
+fi
+
+page="$(echo "$1" | sed 's/\./\\./')"
+target=$(ninja -C "@BUILD_ROOT@" -t query man/man | grep -E -m1 "man/$page\.[0-9]$" | awk '{print $2}')
+if [ -z "$target" ]; then
+    echo "Cannot find page $1"
+    exit 1
+fi
+ninja -C "@BUILD_ROOT@" "$target"
+exec man "@BUILD_ROOT@/$target"