1 files changed, 28 insertions, 0 deletions
diff --git a/man/man.in b/man/man.in
new file mode 100755
index 0000000..12eb332
--- /dev/null
+++ b/man/man.in
@@ -0,0 +1,28 @@
+#!/bin/sh
+set -e
+
+if [ -z "$1" ]; then
+    echo "Use: $0 page-name (with no section suffix)"
+    exit 1
+fi
+
+# make sure the rules have been regenerated (in case man/update-man-rules was just run)
+ninja -C "@BUILD_ROOT@" version.h
+
+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"
+
+fullname="@BUILD_ROOT@/$target"
+redirect="$(sed -n -r '1 s|^\.so man[0-9]/(.*)|\1|p' "$fullname")"
+if [ -n "$redirect" ]; then
+    ninja -C "@BUILD_ROOT@" "man/$redirect"
+
+    fullname="@BUILD_ROOT@/man/$redirect"
+fi
+
+exec man "$fullname"