From d4539b4a108d1269f9accdf34ecbd1b8b3453f30 Mon Sep 17 00:00:00 2001 From: gwenn Date: Sat, 8 Jan 2022 12:40:33 +0100 Subject: [PATCH] Remove old script publish-ghp-docs.sh --- publish-ghp-docs.sh | 14 -------------- 1 file changed, 14 deletions(-) delete mode 100755 publish-ghp-docs.sh diff --git a/publish-ghp-docs.sh b/publish-ghp-docs.sh deleted file mode 100755 index 14f358a..0000000 --- a/publish-ghp-docs.sh +++ /dev/null @@ -1,14 +0,0 @@ -#!/bin/bash - -git describe --exact-match --tags $(git log -n1 --pretty='%h') >/dev/null 2>&1 -if [[ $? != 0 ]]; then - echo "Should not publish tags from an untagged commit!" - exit 1 -fi - -cd $(git rev-parse --show-toplevel) -rm -rf target/doc/ -rustup run nightly cargo doc --no-deps --features "backup blob chrono functions limits load_extension serde_json trace" -echo '' > target/doc/index.html -ghp-import target/doc -git push origin gh-pages:gh-pages