From: Loup Vaillant <loup@loup-vaillant.fr>
Date: Tue, 29 Aug 2023 09:12:01 +0000 (+0200)
Subject: Fix /bin/env vs /usr/bin/env vs nothing
X-Git-Url: https://git.codecow.com/?a=commitdiff_plain;h=03fbc677d9912c49b7e363d69523cd4269eead6a;p=Monocypher.git

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 0d36b33..63ef535 100755
--- 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 cc84842..3e9d1a8 100755
--- 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.