Issue #649: Drop the generated doc/Doxyfile when creating a release.

diff --git a/RELEASE_CHECKLIST.txt b/RELEASE_CHECKLIST.txt
index da5d8d7c7501359b77aee6ca18709c4e1f32ab29..8e7061750df0a92d77a9426ee839eaa1fe468c8b 100644 (file)
--- a/RELEASE_CHECKLIST.txt
+++ b/RELEASE_CHECKLIST.txt
@@ -81,6 +81,7 @@ Generate the doxygen documentation:
 
     (cd ../distcheck && make doc)
     cp -r -p ../distcheck/doc/{html,Doxyfile} doc/.
+       rm doc/Doxyfile   # Remove generated file w/ hardcoded paths
     git add -f doc
     git commit doc -m "Generate docs for the ${release} release"