Golf scripts/build_docs.sh (#43)

Author: b-mehta

scripts/build_docs.sh

@@ -1,9 +1,11 @@
 # Build HTML documentation for add-combi
 # The output will be located in docs/build
 
-# Template lakefile.toml
-template() {
-  cat <<EOF
+# Create a temporary docbuild folder
+mkdir -p docbuild
+
+# Equip docbuild with this template lakefile.toml
+cat << EOF > docbuild/lakefile.toml
 name = "docbuild"
 reservoir = false
 version = "0.1.0"
@@ -16,18 +18,8 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "TOOLCHAIN"
+rev = "$(< lean-toolchain cut -f 2 -d: )"
 EOF
-}
-
-# Create a temporary docbuild folder
-mkdir -p docbuild
-
-# Equip docbuild with the template lakefile.toml
-template > docbuild/lakefile.toml
-
-# Substitute the toolchain from lean-toolchain into docbuild/lakefile.toml
-sed -i s/TOOLCHAIN/`grep -oP 'v4\..*' lean-toolchain`/ docbuild/lakefile.toml
 
 # Fetch the docs cache if it exists
 mkdir -p website/docs