diff --git a/nix/lean-dev.in b/nix/lean-dev.in index 9bee622ee6..02849ad55f 100644 --- a/nix/lean-dev.in +++ b/nix/lean-dev.in @@ -1,6 +1,6 @@ #!@bash@/bin/bash -set -euxo pipefail +set -euo pipefail root="." # find package root