From 03fbc677d9912c49b7e363d69523cd4269eead6a Mon Sep 17 00:00:00 2001 From: Loup Vaillant Date: Tue, 29 Aug 2023 11:12:01 +0200 Subject: [PATCH] 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. --- change-prefix.sh | 2 +- doc/doc_check.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/change-prefix.sh b/change-prefix.sh index 0d36b33f..63ef5356 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 cc848427..3e9d1a83 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.