add script to push docs (will be tested soon)

[rust-101.git] / push-docs

diff --git a/push-docs b/push-docs
new file mode 100644 (file)
index 0000000..7a6dc60
--- /dev/null
+++ b/push-docs
@@ -0,0 +1,9 @@
+#!/bin/bash
+set -e
+
+cd "$(dirname "$0"))"
+./pycco-rs src/*.rs
+cd docs
+git add .
+git commit -m "semi-auto-update of the documentation"
+git push