From 135432b32976453da6eb80dcea0d9927683ac47d Mon Sep 17 00:00:00 2001
From: Shish <shish@shishnet.org>
Date: Fri, 6 Mar 2020 13:44:51 +0000
Subject: [PATCH] don't crash when docs are missing

---
 ext/ext_manager/theme.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ext/ext_manager/theme.php b/ext/ext_manager/theme.php
index 1a0c2e4f..e9235f46 100644
--- a/ext/ext_manager/theme.php
+++ b/ext/ext_manager/theme.php
@@ -109,7 +109,7 @@ class ExtManagerTheme extends Themelet
             $author,
             ($info->version ? emptyHTML(BR(), B("Version"), $info->version) : null),
             ($info->link ? emptyHTML(BR(), B("Home Page"), A(["href"=>$info->link], "Link")) : null),
-            P(rawHTML($info->documentation)),
+            P(rawHTML($info->documentation ?? "(This extension has no documentation)")),
             // <hr>,
             P(A(["href"=>make_link("ext_manager")], "Back to the list"))
         );