diff options
| -rw-r--r-- | tools/build/make_check/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/build/make_check/Makefile b/tools/build/make_check/Makefile index 4c2389a..e57e70c 100644 --- a/tools/build/make_check/Makefile +++ b/tools/build/make_check/Makefile @@ -262,7 +262,7 @@ shell_1_csh: .if make(shell_1_sh) .SHELL: name="sh" shell_1_sh: - @ps -ax -opid,command | awk '$$1=="'$$$$'" { print $$2 }' | grep -q '^/bin/sh$$' + @ps -ax -opid,command | awk '$$1=="'$$$$'" { print $$2 }' | grep -E -q '^(/bin/)?sh$$' .endif .if make(shell_2) |
