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

chore: Nix: remove Leanpkg from stage 0

Browse source
This commit is contained in:
Sebastian Ullrich 2021-09-20 16:26:51 +02:00
parent d3eb5deeea
commit f49d05bd76
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
nix/bootstrap.nix
View file

@ -141,7 +141,7 @@ rec {
'';
};
update-stage0 =
let cTree = symlinkJoin { name = "cs"; paths = [ Init.cTree Std.cTree Lean.cTree Leanpkg.cTree ]; }; in
let cTree = symlinkJoin { name = "cs"; paths = map (l: l.cTree) stdlib; }; in
writeShellScriptBin "update-stage0" ''
CSRCS=${cTree} CP_PARAMS="--dereference --no-preserve=all" ${../script/update-stage0}
'';