Fix /bin/env vs /usr/bin/env vs nothing

There's no such thing as /bin/env, though I let that slip by because my
distro redirects /bin to /usr/bin.

I believe "#! /bin/sh" is even more standard that "#! /usr/bin/env sh",
and that's what I used everywhere anyway.

diff --git a/change-prefix.sh b/change-prefix.sh
index 0d36b33fca1f4ebead73491d771e6e59245747fa..63ef53566ad1974ddb06315c96f26a59ad680502 100755 (executable)
--- a/change-prefix.sh
+++ b/change-prefix.sh
@@ -1,4 +1,4 @@
-#! /usr/bin/env sh
+#! /bin/sh
 
 # This file is dual-licensed.  Choose whichever licence you want from
 # the two licences listed below.

diff --git a/doc/doc_check.py b/doc/doc_check.py
index cc848427691e84cf84696214e15b5a555d7cc7de..3e9d1a83724e500b153b9aa52bc832282c5fbde0 100755 (executable)
--- a/doc/doc_check.py
+++ b/doc/doc_check.py
@@ -1,4 +1,4 @@
-#! /bin/env python3
+#! /usr/bin/env python3
 
 # This file is dual-licensed.  Choose whichever licence you want from
 # the two licences listed below.