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 09d0ab45be..a67e894ef6 100644 --- a/make_ext.pl +++ b/make_ext.pl @@ -531,7 +531,7 @@ else if test ! -f Makefile ; then echo "Warning: No Makefile!" fi - make -s $clean_target MAKE='@make' @pass_through + @make $clean_target MAKE='@make' @pass_through fi cd $return_dir EOS |