From 3121c10c737a30d1288ad3955f9105dcb193df73 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Mon, 6 Nov 2023 12:20:00 +0000
Subject: 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.
---
 .gitlab-ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to '.gitlab-ci.yml')

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:
-- 
cgit v1.2.3-54-g00ecf