From 02e917793e07d480ee09bda7b51210b976b47e6d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 25 May 2021 15:24:31 +0200 Subject: [PATCH] chore: Nix: default `lean-dev` to Lean w/ package Restores `lean4-diff-test-file` and similar functionality --- nix/lean-dev.in | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/nix/lean-dev.in b/nix/lean-dev.in index efccb33677..e224a00787 100644 --- a/nix/lean-dev.in +++ b/nix/lean-dev.in @@ -10,7 +10,17 @@ while [[ "$root" != / ]]; do done # fall back to initial package if not in package [[ ! -f "$root/flake.nix" ]] && root="@srcRoot@" -target="$root#lean" + +# use Lean w/ package unless in server mode (which has its own LEAN_PATH logic) +target="$root#lean-package" +for arg in "$@"; do + case $arg in + --server | --worker) + target="$root#lean" + ;; + esac +done + args=(-- "$@") # HACK: use stage 0 instead of 1 inside Lean's own `src/` [[ -d Lean && -f ../flake.nix ]] && target="@srcTarget@" && args=@srcArgs@