From a51e415b730013e80fd61b48ff0f90050aa4812c Mon Sep 17 00:00:00 2001
From: Joachim Ansorg <github@ja-dev.eu>
Date: Fri, 27 Dec 2024 17:32:31 +0100
Subject: [PATCH 1/2] Allow to manually execute a GitHub Actions workflow

---
 .github/workflows/CI.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml
index 092187d..eee3ad5 100644
--- a/.github/workflows/CI.yml
+++ b/.github/workflows/CI.yml
@@ -1,6 +1,7 @@
 name: "bashdb CI"
 on:
   push:
+  workflow_dispatch:
 
 jobs:
   tests:

From 8306353df134fc568fa9dd731d7e49a485934b7a Mon Sep 17 00:00:00 2001
From: Joachim Ansorg <github@ja-dev.eu>
Date: Fri, 27 Dec 2024 18:09:56 +0100
Subject: [PATCH 2/2] Docker bash:4.4 has bash at /usr/local/bin

---
 check-prefix.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/check-prefix.sh b/check-prefix.sh
index d1ad285..d575089 100755
--- a/check-prefix.sh
+++ b/check-prefix.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/usr/bin/env bash
 if [[ $# != 2 ]]; then
     echo  >&2 "Usage $0 BASH_PROGRAM PREFIX"
     exit 3