From 73ae39313dd09a3ea885a1a2f75340e0d04e2f46 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 7 Dec 2020 15:06:49 +0100 Subject: [PATCH] fix: Nix: better stage 0 detection --- nix/lean-dev.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/nix/lean-dev.in b/nix/lean-dev.in index d9774e5372..be8e76b338 100644 --- a/nix/lean-dev.in +++ b/nix/lean-dev.in @@ -42,8 +42,8 @@ done [[ "$root" == / ]] && root="@srcRoot@" deps="$(echo -n "$input" | nix run "$root#print-lean-deps" 2> /dev/null)" attrPath="check-mod" -# HACK: use stage 0 instead of 0 inside Lean's own `src/` -[[ -d "$root/src/Lean" && "$inputFile" == "$root/src/"* ]] && attrPath="stage0check-mod" +# HACK: use stage 0 instead of 1 inside Lean's own `src/` +[[ -d "$root/src/Lean" && "$(realpath "$inputFile")" == "$root/src/"* ]] && attrPath="stage0check-mod" for dep in $deps; do attrPath="$attrPath.\"$dep\"" done