191 | | extensions which are considered when deciding whether a file has been |
192 | | already downloaded. When an alias is specified as above, |
193 | | a file ending in ''_1'' will be considered already |
194 | | downloaded, and its retrieval skipped, if a file |
195 | | with a similar name but ending in |
196 | | ''_1.vel'' or ''_1.vel.gz'' is present in the |
197 | | retrieve directory. |
| 191 | extensions which serves two purposes: |
| 192 | * ''automatic renaming'': retrieved files will receive the extension |
| 193 | listed as a first element; |
| 194 | * ''avoiding duplicate retrievals'': they are considered when deciding whether a file has been |
| 195 | already downloaded (equivalence classes). For example, with the alias above, |
| 196 | a result file called ''xx_1'' will NOT be retrieved if one of the following files is |
| 197 | present in the download directory: |
| 198 | ''xx_1.vel'', ''xx_1.vel.gz''. |