fix: JS syntax (#259)

leanprover · Dec 22, 2024 · 7d3a46e · 7d3a46e
1 parent bc5c64e
commit 7d3a46e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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}`);
   }
 })()"#