Fix Verso path [annotate]

utensil · Oct 28, 2024 · ce2a6e1 · ce2a6e1
1 parent f9e075d
commit ce2a6e1
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 5 deletions.
diff --git a/.github/workflows/lean4.yml b/.github/workflows/lean4.yml
@@ -50,6 +50,7 @@ jobs:
             shared:
               - added|modified: '.github/workflows/lean4.yml'
               - added|modified: 'lean4-xp-kit/**/*'
+              - added|modified: 'justfile'
             lean4:
               - added|modified: 'lean4/**/*'
             duper:
@@ -134,7 +135,7 @@ jobs:
           popd
 
           pushd lean4-verso-xp
-          just doc
+          just vsgen
           popd
 
           just pages lean4

diff --git a/justfile b/justfile
@@ -54,9 +54,11 @@ up *NAME:
     lake -R build
 
 [no-cd]
-doc:
+vsgen:
     lake -R exe mkVersoDoc
+    rm -rf dist
+    mv _out/html-multi dist
 
 [no-cd]
-vdoc: doc
-    open dist/html-multi/index.html
+vs: vsgen
+    open dist/index.html
diff --git a/lean4-verso-xp/Main.lean b/lean4-verso-xp/Main.lean
@@ -7,7 +7,7 @@ def main :=
   manualMain (%doc VersoXp) (config := config)
 where
   config := {
-    destination := "dist",
+    -- destination := "dist",
     extraFiles := [("static", "static")],
     -- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
     -- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],