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

chore: Nix: fix nix run

Browse source
This commit is contained in:
Sebastian Ullrich 2020-11-22 17:08:34 +01:00
parent e167085429
commit fc6ddcef94
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
nix/bootstrap.nix
View file

@ -62,7 +62,8 @@ rec {
inherit (Lean) emacs-dev emacs-package;
mods = Init.mods // Std.mods // Lean.mods;
lean = stdenv.mkDerivation {
name = "lean-${desc}";
# can't use `${desc}` here without breaking `nix run`...
name = "lean";
buildCommand = ''
mkdir -p $out/bin $out/lib/lean
ln -sf ${leancpp}/lib/lean/* ${Init.staticLib}/* ${Init.modRoot}/* ${Lean.staticLib}/* ${Lean.modRoot}/* ${Std.staticLib}/* ${Std.modRoot}/* $out/lib/lean/