From c8d390dbc5a749af533f1ec05de2d5b6f37fa156 Mon Sep 17 00:00:00 2001
From: Jacky Zhao <j.zhao2k19@gmail.com>
Date: Thu, 28 Apr 2022 20:45:29 +0000
Subject: [PATCH] fix: always hide popover on mobile (fixes #104)

---
 assets/js/search.js |    2 +-
 1 files changed, 1 insertions(+), 1 deletions(-)

diff --git a/assets/js/search.js b/assets/js/search.js
index facebe5..0aacb5f 100644
--- a/assets/js/search.js
+++ b/assets/js/search.js
@@ -131,7 +131,7 @@
   }
 
   const redir = (id, term) => {
-    window.location.href = BASE_URL + `${id}#:~:text=${encodeURIComponent(term)}`
+    window.location.href = `${BASE_URL}${id}#:~:text=${encodeURIComponent(term)}/`
   }
 
   const formatForDisplay = id => ({

--
Gitblit v1.10.0