diff options
Diffstat (limited to 'infrastructure/makedistribution.pl')
| -rwxr-xr-x | infrastructure/makedistribution.pl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/infrastructure/makedistribution.pl b/infrastructure/makedistribution.pl index 669f5de6..823aba38 100755 --- a/infrastructure/makedistribution.pl +++ b/infrastructure/makedistribution.pl @@ -82,6 +82,15 @@ sub copy_from_list { $no_license{$dst} = 1; } + elsif($src eq 'RUN') + { + print "Running $dst...\n"; + if(system($dst) != 0) + { + print "Error running $dst. Aborting.\n"; + exit(1); + } + } elsif(-d $src) { $modules_included{$_} = 1; |