Initial commit - update DOCUMENTATION_OPTIONS before removing dev docs

dev/release/post-08-docs.sh

@@ -60,6 +60,21 @@ for versioned_path in docs/*.0/; do
   versioned_paths+=(${versioned_path})
   rm -rf ${versioned_path}
 done
+
+# Update DOCUMENTATION_OPTIONS.show_version_warning_banner
+# for dev docs (becoming stable docs)
+pushd docs/dev
+find ./ \
+  -type f \
+  -exec \
+    sed -i.bak \
+      -e "s/DOCUMENTATION_OPTIONS.show_version_warning_banner = true/DOCUMENTATION_OPTIONS.show_version_warning_banner = false/g" \
+      {} \;
+find ./ -name '*.bak' -delete
+popd
+git add docs/dev
+git commit -m "[Website] Update warning banner for dev docs"
+
 # add to list and remove dev docs
 versioned_paths+=("docs/dev/")
 rm -rf docs/dev/