diff options
author | Chris Wilson <chris+github@qwirx.com> | 2007-03-04 22:59:22 +0000 |
---|---|---|
committer | Chris Wilson <chris+github@qwirx.com> | 2007-03-04 22:59:22 +0000 |
commit | 1953c377019e084e41898d4831f71c651839e82d (patch) | |
tree | c693e4a72cea94901cec944f3fcc74a71e3b3d3b /infrastructure/makeparcels.pl.in | |
parent | ba61e64d38900324728cc028766564fe2d021057 (diff) |
Fix make error when optional file doesn't exist (refs #3, merges [1098])
Diffstat (limited to 'infrastructure/makeparcels.pl.in')
-rwxr-xr-x | infrastructure/makeparcels.pl.in | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/infrastructure/makeparcels.pl.in b/infrastructure/makeparcels.pl.in index e70dcf29..a8eceb8a 100755 --- a/infrastructure/makeparcels.pl.in +++ b/infrastructure/makeparcels.pl.in @@ -123,7 +123,8 @@ for my $parcel (@parcels) { if ($optional) { - print MAKE "\ttest -r $name && cp $name $dir\n"; + print MAKE "\ttest -r $name " . + "&& cp $name $dir || true\n"; } else { |