Revert "Auxiliary commit to revert individual files from 4608b5e"

dkijania · dkijania · commit 7e023b2dc2c3 · 2024-11-13T14:06:24.000+01:00
This reverts commit c95524dc777d273bc8fdc627a424e98d525565a8.
diff --git a/maintenance/gen_deps.sh b/maintenance/gen_deps.sh
@@ -1,4 +1,4 @@
-#!/bin/bash
+#!/bin/sh
 set -e -o pipefail
 maintenance_dir="$(realpath $(dirname $0))"
 [ "$(which dune-deps)" != '' ] || (echo 'missing required executable "dune-deps"; try `opam install dune-deps`' && exit 1)

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-#!/bin/bash`
	`1`	`+#!/bin/sh`
`2`	`2`	`set -e -o pipefail`
`3`	`3`	`maintenance_dir="$(realpath $(dirname $0))"`
`4`	`4`	[ "$(which dune-deps)" != '' ] \|\| (echo 'missing required executable "dune-deps"; try `opam install dune-deps`' && exit 1)