max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: Nix: better stage 0 detection

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-07 15:06:49 +01:00
parent b12be950bf
commit 73ae39313d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
nix/lean-dev.in
View file

@ -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