remove comment that's about to become obsolete

diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh
index be9a1262fe205a4ab7bcafbfed85b84a0caabe6a..cdc2eb39c77565903ba8efa41297203e0ca19be5 100755 (executable)
--- a/Doc/tools/push-docs.sh
+++ b/Doc/tools/push-docs.sh
@@ -64,7 +64,6 @@ if [ "$1" ] ; then
 fi
 
 if [ "$DOCTYPE" = 'maint' ] ; then
-    # 'maint' is a symlink
     DOCTYPE='maint23'
 fi