| 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''. |