Release scripts: small changes to reduce intermittent failures

Browse Source

-don't check exit status of wget in the trigger_pdfgen script;
 it was exiting with non-0 status even though the pdf generation
 was being triggered correctly

-introduce a delay after filtering the git history to allow HEAD
 to be properly reset

-re-enable sanity checks in filter_stable and source_release scripts
 that had temporarily been disabled while the new protected repository
 was being set up

...

This commit is contained in:

David Roazen 2013-03-19 00:53:47 -04:00

parent 7ab7c873a1

commit 532efad8cd

Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL

Show Stats Download Patch File Download Diff File Expand all files Collapse all files

Diff Content Not Available