Merge pull request #7612 from TheElectronWill/redesign-dottydoc-theme

Fix #7595: Redesign dottydoc theme

Author: smarter

doc-tool/bootstrap-theme/build.sh

@@ -1,6 +1,16 @@
 #!/bin/sh
 cd "$(dirname "$0")"
+if [ ! -d "node_modules" ]; then
+  npm install
+fi
 npm run build
-echo "Copying css file..."
+echo "Copying CSS result..."
 cp target/bootstrap.min.css ../resources/css/bootstrap.min.css
-echo "Bootstrap css updated."
+
+# Update the generated website without running sbt
+gen_dir=../../docs/_site/css
+if [ -d "$gen_dir" ]; then
+  cp ../resources/css/* $gen_dir/
+fi
+
+echo "Bootstrap CSS updated."

doc-tool/bootstrap-theme/package-lock.json

@@ -14,7 +14,7 @@
     "autoprefixer": "^9.6.1",
     "bootstrap": "^4.3.1",
     "cssnano": "^4.1.10",
-    "node-sass": "^4.12.0",
+    "node-sass": "^4.13.0",
     "postcss-cli": "^6.1.3"
   }
 }