diff options
Diffstat (limited to 'make_ext.pl')
| -rw-r--r-- | make_ext.pl | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/make_ext.pl b/make_ext.pl index 98ed3cc6e1..0c877fc9ea 100644 --- a/make_ext.pl +++ b/make_ext.pl @@ -124,7 +124,7 @@ my @make = split ' ', $1 || $Config{make} || $ENV{MAKE}; if ($target eq '') { die "make_ext: no make target specified (eg all or clean)\n"; -} elsif ($target !~ /(?:^all|clean)$/) { +} elsif ($target !~ /^(?:all|clean|distclean|realclean|veryclean)$/) { # for the time being we are strict about what make_ext is used for die "$0: unknown make target '$target'\n"; } |