[docs] add push_with_docs script

scripts/configure_docs_url.sh

@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -Eeuo pipefail
+
+ROOT="$(git rev-parse --show-toplevel)"
+cd "$ROOT"
+
+if [[ $# -gt 1 ]]; then
+    echo "usage: $0 [docs-site-url]" >&2
+    exit 2
+fi
+
+if [[ $# -eq 1 ]]; then
+    git config meanas.docsSiteUrl "$1"
+    echo "Configured meanas.docsSiteUrl=$1"
+    exit 0
+fi
+
+CURRENT_URL="$(git config --get meanas.docsSiteUrl || true)"
+if [[ -n "$CURRENT_URL" ]]; then
+    echo "$CURRENT_URL"
+else
+    echo "meanas.docsSiteUrl is not configured" >&2
+    exit 1
+fi