Mark the notice about the new development version of the docs as not needing

to be archived.  Most of these are pretty bland.  ;-)

diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh
index 389f7bb0406ff33710af4810ac0e6008f5151c05..ab789e6388fb2354452e4edcb7fc49fd7345f2f7 100755 (executable)
--- a/Doc/tools/push-docs.sh
+++ b/Doc/tools/push-docs.sh
@@ -78,6 +78,7 @@ if $ANNOUNCE ; then
 To: $ADDRESSES
 From: "Fred L. Drake" <fdrake@acm.org>
 Subject: [$DOCLABEL doc updates]
+X-No-Archive: yes
 
 The $DOCLABEL version of the documentation has been updated: