more version cruft

diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh
index 28a4b31589d1cf61bfab69224b28601b8af21814..9e5973eb131d1bccd6fbe76ee8a3024387632f0d 100755 (executable)
--- a/Doc/tools/push-docs.sh
+++ b/Doc/tools/push-docs.sh
@@ -85,6 +85,11 @@ if [ "$1" ] ; then
     shift
 fi
 
+if [ "$DOCTYPE" = 'maint' ] ; then
+    # 'maint' is a symlink
+    DOCTYPE='maint24'
+fi
+
 START="`pwd`"
 MYDIR="`dirname $0`"
 cd "$MYDIR"