| commit | 36bcf9b94f8cbec99881f07225f4c682a7fecbe2 | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Tue Mar 06 22:43:06 2001 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Tue Mar 06 22:43:06 2001 +0000 |
| tree | 82a3d38d59e32bca7c64f0ec5122ebe9079d3aef | |
| parent | cbe7b1c93e1c428356e48eb5512bdffd20ceca94 [diff] |
Re-try the file copy once if it fails. This works around an obscure and non-reproducibe bug in GUSI.