From f31c03a0cc74a67a2a0e456bd2aa1bacb02b2b52 Mon Sep 17 00:00:00 2001
From: Bart Van Assche <bvanassche@acm.org>
Date: Fri, 15 May 2020 11:48:36 -0700
Subject: [PATCH] scripts/list-source-files: Use /bin/sh as interpreter instead
 of bash

---
 scripts/list-source-files | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/list-source-files b/scripts/list-source-files
index 09550eed8..3ab87a93f 100755
--- a/scripts/list-source-files
+++ b/scripts/list-source-files
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 
 list_source_files() {
   local d r