diff options
| author | Ian Jackson <ijackson@chiark.greenend.org.uk> | 2023-11-06 12:20:00 +0000 |
|---|---|---|
| committer | Ian Jackson <ijackson@chiark.greenend.org.uk> | 2023-11-06 12:40:14 +0000 |
| commit | 3121c10c737a30d1288ad3955f9105dcb193df73 (patch) | |
| tree | 3a2ea674921aee44d104ef0c33f5bedcc8402938 | |
| parent | 3fb917d86aad672b63005ef44e4936fe1564a8ff (diff) | |
| download | torspec-3121c10c737a30d1288ad3955f9105dcb193df73.tar.gz torspec-3121c10c737a30d1288ad3955f9105dcb193df73.zip | |
Remove language file extension from bin/*
Putting ".sh" or ".py" on the end of scripts is an antipattern.
It makes it inconvenient to change the implementation language.
Change all call sites.
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rwxr-xr-x | bin/build_html (renamed from bin/build_html.sh) | 4 | ||||
| -rwxr-xr-x | bin/check_index | 2 | ||||
| -rwxr-xr-x | bin/make_redirects (renamed from bin/make_redirects.py) | 0 | ||||
| -rwxr-xr-x | bin/reindex (renamed from bin/reindex.py) | 0 | ||||
| -rw-r--r-- | spec/README.md | 2 |
6 files changed, 5 insertions, 5 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 687baca..f01e598 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -8,7 +8,7 @@ build: - cargo install mdbook - apt-get update && apt-get install -y git python3 python3-yaml - ./bin/check_index - - ./bin/build_html.sh + - ./bin/build_html - mv html public artifacts: paths: diff --git a/bin/build_html.sh b/bin/build_html index 09b92e2..026c525 100755 --- a/bin/build_html.sh +++ b/bin/build_html @@ -6,9 +6,9 @@ set -e -u -o pipefail -x TOPLEVEL=$(realpath $(dirname "$0"))/.. cd "${TOPLEVEL}" -./bin/reindex.py +./bin/reindex -./bin/make_redirects.py +./bin/make_redirects cd "${TOPLEVEL}/mdbook/spec" $MDBOOK build diff --git a/bin/check_index b/bin/check_index index 77bdb02..a2e8c4f 100755 --- a/bin/check_index +++ b/bin/check_index @@ -14,7 +14,7 @@ if ! git diff --quiet ; then fi cd "$TOPLEVEL/" -./bin/reindex.py +./bin/reindex if ! git diff --quiet ; then echo "Proposal index is not up-to-date. Run ./reindex.py to regenerate it." >&2 diff --git a/bin/make_redirects.py b/bin/make_redirects index ea8ea3b..ea8ea3b 100755 --- a/bin/make_redirects.py +++ b/bin/make_redirects diff --git a/bin/reindex.py b/bin/reindex index 57ac403..57ac403 100755 --- a/bin/reindex.py +++ b/bin/reindex diff --git a/spec/README.md b/spec/README.md index 0686384..9633944 100644 --- a/spec/README.md +++ b/spec/README.md @@ -55,7 +55,7 @@ The chapter structure as a whole is defined in a special file called documentation][mdbook documentation] for more information. You can build the website locally to see how it renders. To do this, -just install mdbook and run the `./bin/build_html.sh` script. (You will +just install mdbook and run the `./bin/build_html` script. (You will need to have mdbook installed to do this.) We have started a [style guide](./STYLE.md) for writing new parts of |