Skip to content

Commit

Permalink
Revert "Auxiliary commit to revert individual files from 4608b5e"
Browse files Browse the repository at this point in the history
This reverts commit c95524dc777d273bc8fdc627a424e98d525565a8.
  • Loading branch information
dkijania committed Nov 13, 2024
1 parent 916ec36 commit 7e023b2
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion maintenance/gen_deps.sh
Original file line number Diff line number Diff line change
@@ -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)
Expand Down

0 comments on commit 7e023b2

Please sign in to comment.