From fdad29770bc0472b917f1ea91cb5301fb9d896ab Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 28 May 2021 15:31:20 +0200
Subject: [PATCH] chore: Nix: expose vscode & extension without lean-dev
 wrapper

---
 nix/packages.nix | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/nix/packages.nix b/nix/packages.nix
index c41e82a59f..87761b0d7e 100644
--- a/nix/packages.nix
+++ b/nix/packages.nix
@@ -101,7 +101,7 @@ let
     dontInstall = true;
   };
 in {
-  inherit cc lean4-mode buildLeanPackage llvmPackages;
+  inherit cc lean4-mode buildLeanPackage llvmPackages vscode-lean4;
   lean = lean.stage1;
   stage0print-paths = lean.stage1.Leanpkg.print-paths;
   HEAD-as-stage0 = (lean.stage1.Lean.overrideArgs { srcTarget = "..#stage0-from-input.stage0"; srcArgs = "(--override-input lean-stage0 ..\?rev=$(git rev-parse HEAD) -- -Dinterpreter.prefer_native=false \"$@\")"; });
@@ -116,5 +116,6 @@ in {
     "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S"
   '';
   mdbook = lean-mdbook;
+  vscode = lean-vscode;
   inherit doc doc-test;
 } // lean.stage1.Lean // lean.stage1 // lean