ghwikipp: If a document ends in ".md" or ".mediawiki", redirect to page without it.

SDL Commits
1 
From 41c3c0370ea6240b8278a77718bb1263b20abfff Mon Sep 17 00:00:00 2001
From: "Ryan C. Gordon" <[EMAIL REDACTED]>
Date: Tue, 6 May 2025 04:22:34 +0000
Subject: [PATCH] If a document ends in ".md" or ".mediawiki", redirect to page
 without it.

This lets things in the headers link to the actual file, but it will still
work when bridged to the wiki.
---
 index.php | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/index.php b/index.php
index 7d5f000..70711d4 100644
--- a/index.php
+++ b/index.php
@@ -1232,6 +1232,13 @@ function sort_search_results($a, $b)
             $reqargs[0] = $document;
         }
     }
+
+    // Drop Markdown and MediaWiki file extensions, so bridged documentation can refer to files and have it work on the wiki, too.
+    $document = preg_replace('/\.(md|mediawiki)$/', '', $document, -1, $count);
+    if ($count == 1) {
+        $reqargs[0] = $document;
+        redirect("$base_url/" . implode('/', $reqargs));
+    }
 }
 
 $operation = ($reqargcount >= 2) ? $reqargs[1] : 'view';