diff options
Diffstat (limited to 'infrastructure')
| -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 { |