diff --git a/tool/ports/current b/tool/ports/current index 9403d4c1b3..2fb323f0b8 100755 --- a/tool/ports/current +++ b/tool/ports/current @@ -1,4 +1,4 @@ -#!/usr/bin/make -f +#!/usr/bin/make -sf # # \brief Tool for printing current contrib directory of port