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