From 7d3a46ef38a48b9a5597fa543df918351a1876d1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Sun, 22 Dec 2024 12:58:38 +0100 Subject: [PATCH] fix: JS syntax (#259) --- src/verso-manual/VersoManual/Html.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean index e809f65..27c9408 100644 --- a/src/verso-manual/VersoManual/Html.lean +++ b/src/verso-manual/VersoManual/Html.lean @@ -469,7 +469,7 @@ configuration. But not all hosts allow this to happen, and most clients have JS def addSlashJs : String := r#"(function(){ const {protocol:proto, host:hostName, pathname:path, search:srch, hash:hsh} = window.location; - if !(path.endsWith("/") || path.endsWith(".html")) { + if (!(path.endsWith("/") || path.endsWith(".html"))) { window.location.replace(`${proto}//${hostName}${path}/${srch}${hsh}`); } })()"#