Finished page title generation (#3650)

Fixed #3359 The live pages deployed on: https://kcatma.github.io/k Co-authored-by: Yiyi Wang <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Sep 22, 2023 · 92d3858 · 92d3858
1 parent 3287f0f
commit 92d3858
Show file tree

Hide file tree

Showing 4 changed files with 102 additions and 470 deletions.
diff --git a/web/build-html.js b/web/build-html.js
@@ -36,6 +36,7 @@ generatePagesFromMarkdownFiles({
   },
   displayCodeBlockSelectors: true,
   displayCodeBlockLineNumbers: true,
+  defaultPageTitle: "K",
 });
 generatePagesFromMarkdownFiles({
   globPattern: path.resolve(__dirname, "./pages/") + "/**/*.md",
@@ -52,6 +53,7 @@ generatePagesFromMarkdownFiles({
   },
   displayCodeBlockSelectors: true,
   displayCodeBlockLineNumbers: true,
+  defaultPageTitle: "K",
 });
 generatePagesFromMarkdownFiles({
   globPattern: path.resolve(__dirname, "../docs/") + "/*.md",
@@ -68,6 +70,7 @@ generatePagesFromMarkdownFiles({
   },
   displayCodeBlockSelectors: true,
   displayCodeBlockLineNumbers: true,
+  defaultPageTitle: "K",
 });
 
 fs.copyFileSync(

diff --git a/web/k-web-theme b/web/k-web-theme
+2 −0		index.js
+95 −466		package-lock.json
+5 −6		package.json