diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index 9ff94f26c8..d2437ba931 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -185,7 +185,6 @@ in rec { isExecutable = true; srcRoot = fullSrc; # use root flake.nix in case of Lean repo inherit bash nix srcTarget srcArgs; - leanpkg = lean; }; lean-dev = symlinkJoin { name = "lean-dev"; paths = [ lean-bin-dev leanpkg-dev ]; }; emacs-dev = makeEmacsWrapper "emacs-dev" lean-dev; diff --git a/nix/leanpkg-dev.in b/nix/leanpkg-dev.in index 0a5b6d6385..75e1e3856b 100644 --- a/nix/leanpkg-dev.in +++ b/nix/leanpkg-dev.in @@ -2,7 +2,7 @@ set -euo pipefail -[[ $# -gt 0 && "$1" == print-paths && ( -f flake.nix || -d Lean && -f ../flake.nix || ! -f leanpkg.toml ) ]] || exec @leanpkg@/bin/leanpkg "$@" +[[ $# -gt 0 && "$1" == print-paths ]] || { echo "This is just a simple Nix adapter for `leanpkg print-paths`. Please use the `leanpkg` attribute for the real thing."; exit 1; } shift deps="$@" root=. @@ -15,6 +15,6 @@ args=() for dep in $deps; do target="$target.\"$dep\"" done -# -v only has "built ...", but "-vv" is a bit too verbose echo "Building dependencies..." >&2 +# -v only has "built ...", but "-vv" is a bit too verbose @nix@/bin/nix run "$target" ${args[*]} -v