diff --git a/.gitignore b/.gitignore index 69fa449dd..86e8c4aa9 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ _build/ +_deployed +_deployed.old diff --git a/_static/syncthing.css b/_static/syncthing.css index a4b07c265..64d3cd83b 100644 --- a/_static/syncthing.css +++ b/_static/syncthing.css @@ -1,7 +1,11 @@ .rst-content p, .rst-content p.admonition-title, .rst-content li, .rst-content table.docutils td, -.rst-content table.docutils th, .rst-content code, .rst-content div[class^='highlight'] pre { - font-size: 14pt; - line-height: 1.35; +.rst-content table.docutils th { + font-size: 120%; + line-height: 1.4; +} +.rst-content code, .rst-content div[class^='highlight'] pre { + font-size: 110%; + line-height: 1.4; } .rst-content li { margin-bottom: 0.5em; diff --git a/deploy.sh b/deploy.sh index 2244ac710..b7dbb90a5 100755 --- a/deploy.sh +++ b/deploy.sh @@ -1,4 +1,11 @@ #!/bin/sh +set -euo pipefail -git pull && rm -fr _build && make html +git pull +rm -fr _build +make html + +rm -rf _deployed.old +[ -d _deployed ] && mv _deployed _deployed.old || true +mv _build _deployed