From 4359b113751c34e9648243d334c2d838829bcab5 Mon Sep 17 00:00:00 2001 From: mhuisi Date: Fri, 10 Nov 2023 18:11:15 +0100 Subject: [PATCH] chore: rename "install elan" button --- README.md | 4 ++-- docs/bootstrapping.md | 2 +- vscode-lean4/media/install-elan.png | Bin 4806 -> 0 bytes vscode-lean4/media/install-lean.png | Bin 0 -> 9455 bytes vscode-lean4/src/utils/leanInstaller.ts | 2 +- 5 files changed, 4 insertions(+), 4 deletions(-) delete mode 100644 vscode-lean4/media/install-elan.png create mode 100644 vscode-lean4/media/install-lean.png diff --git a/README.md b/README.md index 8c9cb5e75..d4c7dc22e 100644 --- a/README.md +++ b/README.md @@ -19,9 +19,9 @@ containing the following: 1. Open your file `hello.lean`. 1. If `Lean` is not yet installed on your system you will see a prompt like this: - ![prompt](vscode-lean4/media/install-elan.png) + ![prompt](vscode-lean4/media/install-lean.png) -1. Click the `Install Lean using Elan` option and enter any default options that appear in the terminal window. +1. Click the `Install Lean` option and enter any default options that appear in the terminal window. 1. After this succeeds the correct version of Lean will be installed by `elan` and you should see something like this in the `Lean: Editor` output panel: ``` diff --git a/docs/bootstrapping.md b/docs/bootstrapping.md index 8521aaad8..1c506dbbd 100644 --- a/docs/bootstrapping.md +++ b/docs/bootstrapping.md @@ -16,7 +16,7 @@ yet and in that case `getLeanVersion` calls `testLeanVersion` on the ![prompt](images/InstallPrompt.png) -If the user clicks `Install Lean using Elan` then this will happen +If the user clicks `Install Lean` then this will happen and elan will be installed in the default location and a stable build of Lean will also be installed. diff --git a/vscode-lean4/media/install-elan.png b/vscode-lean4/media/install-elan.png deleted file mode 100644 index 285b4910878b3638fdda0edb4b128cc188c0151a..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4806 zcmcgwcQ71mw_iyRL5g0&ipc81s?kgIU90Sp=w)@XLXfBtArV2euxg?#tJmnf5rP$U zS9C&@2upNU*>B(P{`1Y;dGEb{-81vldFGjO=9J%WPK>dUF5?xhD*yn1QD5)ADF8s# zMcG?izCf8-8}n{Z7AikeT}?p6;LSD4;gYKcR09C0PM|+^pr)MZeDogr0RUIO{5`08 zP{l|9fXPb#z6SiMEitX;s6c;Vr+J-X|vlmdk5FXaniuf>w6^Mw*0^WV{< zipvwwq!VjqcVLU;zs2terw@v_=*z8~@tF(DI`e+}MFe%Jl-PqfP64^EqgA~iwBKfn z5kh_zihlHKeyj-n+p1wx#UE%lUlNccyNhyG99HYdF8r4!OV!G>E6H4Fei9s7RY9&�l~$zTbi=@2>jCj= z#cl4E@TZ~c#E4MQFDGpBfka3OE#Ns~@y8mPI@Q2cm8~d4lL#g%lE1g7wxP7SwN?F) z_)mok3x(pde}n<{vTJ8cgePlTBWbijFl!<9_Nn3RvE!ZPWF?Z?pj|pzbzi?yjJ#2d zz%+@sSR8cN=t*N;bPvCi8LrK3PV((|x;_cn{O%<)H90B8HZUu)!bCl)z%nqX?ZjVO z&%twdJ_8r??QJhBs-8r=_>KoTD!RP0*Ht*$8G^pr4xAX4^6_o97O@e9<;H@9OCRMP z@G3~A^lsc#{$mT{uT`w?d-8Lodm(UDK5_NeZI#)c!T3iTQy;HBXbe7q(G-alv|6bq zN;yX;z(ny{BlT9@AwMmLptBj=Y6Xuz(TLnPoM&uKDnlBWul>=c_xt)@B?= zt>;|@>0RR)eOHDPfrBg84n{x6~qD#gm>;-lu+QgC&bcW0463t8Bk4NSk?#Y9>h&n=VX<#P-Pkg)2$ zM-lp3a)pXhHkyd2OgB~zTBjt|I@1XSI~n<1Sm+xjtaO?7>Qbm&$zrT1rM(zo-@oR!onGBrcb;-lz~whgf6?BAc&ni$Pu1_RH;nl+ho z`~z8r=oABdMNZ%NW^*#=DtPnDdVpwKKZN*fKpb{Fnv^??No&kF&QpwWhTVhoyR7XF z+o56cIcJ9WG*F(I?tI#~D%GkPSeQq~-ZYO59YC%LUJAH7V3vkQ`~c=3h;>77S>c{f zm%XP@CpWcCF|YE3J)0MyZ8>;kiStJmoqpSXDZ5tpv^L-5V)Sbwr0FgGWog%!1D2#b z?M=4RUr$E}Fk;4X36f=^iljQ#4{xa8AAuIvwugy|C1FoMKR$_U)%cT#KYuLd2=RNM zR&)8Rdb96O7((lldIrR~-u9WI%h=1d8@#H1_YONm?CCm8yyAsm)lod$=6OFysJ-yV z`Z+YsIVtx5w#r7MErm|#5dDCqb~>cqq%v~=NzqY>^$ zw@&Y#4?GD>oIbIQ?SJwmmAK%fO7;myx%oWa#TcTlRcy?01uZQq-M%(Iv!rS%B4(6E zaMVk47c;rjT+)o>lICgB_sW3ZDG69FYwRedNy{) zFbUg*lDmlBVSb+IUYsL{ld%<#x^4Escg_<4ysW?>oDAq|x)FJ+pmw8MNZ zy;j+80QOheaw_G+->%)7i3|`DQ?hS^xC36wsfey@0hr^n>&*e1KzkSdDd# zLc7@tbAC~!ZKguCS|V8>XZf0OHjho{Az}XAs3q6hT+nnn9Ivw5<4wAI+_B016uu41 z@6=|p0*uX}cc^TB5!@^5MY9r|`eDqtl!0G3`qay1>=)3{d2idK8M(?4nCf0ek|ld4 zw&)R>RDnM%J)vZANX+CfZ1fD9sYQ2Ovn|xz^Q3Do?9U*f!HP%pSKZEb{Mex?BFnG4 z6B7xRt*5uW6ural+OL+&vGHr;Ub>oRzz40KK^7zOaa&IO+|W?!-egx)>a(xmT-r;d zz{-vJu&A7U<{}wV!T|*gzS8xt64O=sannaE>oLCgr+3m8D76?Jf(#R^1fd+4e##piI(7aF7Amwy1C_N z&H4B#U(yE)=XwysLAyb<-EL$K#3UzJv%!wHrj;%9RFl@YfdYXK-2I;R)vQ$fGw2FRgqqa}l%?Q5RrpJ&h8*`_PBfBbnAMSYTxY^!pneEPHC zO$G2Iu>389+D#vFUNUrq+X}S>>f3CZjSU~^+oeI-EVI?9o|aw%-~dGkF=WJY z@K7PABwo8ySzeNYTrlB~VV6?8&|7D79e<(jvSa$CJV`eR$0wKGxwr6PsNHUKNz&bS z7`E>Eb(s$zpaG#D=6~(L^t$sy)9aBN>KNjSbhZ!L*S`o{kJ9kFk$?L+WSUw^Ts@XA zTA%MqHJ%Bv&MEW{!-cxBDNOX4k38G_Uyv6uY&2nte(mF^m7RYn1`XSL=0 z_}Ig=Y;%dZyP_jKSA>2iukA0-^UgpC$xRSO#+Y+==P5~w8|wQAO_+PgJ9z8Ia&JcA z>6sa^UkQ(6aVhdeu*u?dHab4ML0uIj^$6*5p;tzf;wF!fZ>vR4L8C0Hg{&38*T*pv zD~+<11+|}VzQxa(kNXHUyGVfV^yJkH7=JCeVD25Qj%n4sN}oA^F#ze-_fz>@`Bv;? zXm*SB)4m~kRG67TUM4la9|~>|L%BX_RhG|*bwRujHTe+>)FK{ToQ~N1Z6zC%6C$Mhx@c@x|=3Du`rh32gps z{D7s&=)9zgJX_5bWcFN&hhwSNyqI@)5}Mg%eMLgP3yI_QPM#U|xdR$G;%zgIz4DJ-^;-^F z4@JH1KBhWk)gCjCRb!~RMG4RkpyKyf8+T>;G0+{kpPZ{@*QLATs)UNz(4$xCPCnqu zi`Ob*O^!YMrwm_susV1JOb#oCgpiMlN~&zKJQmPShDU=0nUo21(84H*P)Ua8gKDq* zovA)tPx^17S)s*Yve$D-@rcdWfhl1oe~nlcTRGYkN%6R;eYKR5?#cF-6)Zf>U(bCCn3QUY^X)%XZtY;Gsdm-vdbG*@Z=$& zXdl5vM4VLm01@C%ckn+fQ?pjSxvH#vS@vKvtsP2%5ZuJiTRb? z#lHNzs#$Y3Ys^Y?qZUnKZa2vHhS4#n7MbldHG22JhHKehxg}UzTKI zPR9}MN#LoI8C1WG$d>-(v-J1e&USZ+L{vhEM&(lI=o4ecKEflED0447Lt>)k;Wd!+ zeX?lM^ffRn2^*wWDS$r;)T+`j@3F-EW~tX?>^ayPN`Q>%?#phzkK3k)K5Y5vV_K_P z0>wn^uy}0s8IBC0xVhOS>4h5w%J8&0K3*T=MSJV6PrF1@%cMGUy=*pEH)E-YPP7My z;rsdq1v}js>v1xZh6gUQbq}4dx=@$70< zBqq*%`RZ(NrQLRmV$;YXlKLwE7Kk2}Z zY!R??mxWPx&uPjL(eq984LpAYtGP3pDWE3Eb);1$HbSB-+!eQL)!^w@On36q=+@e? zx05v5x~Wn_{Gt<*J5s4|9Oi>?qwE7@ zaT`{6XQcj0aZ9au^cF-vB%;0P)*)MJQj>GIlA<6KQvrkEKcCO$`ZB@d>}(vt+**`C z^mt+ZPI$oZ?A?-_Bj^C0p9R0R$E0gq;lRmafFgJ+K!z9xNx_j zMR|jv|Az5TXRIz52v^cuu>Z#g|F7u(zji*HjguP}?PL@vW3rS}BT*EYIep=tl(UwEGj~DhRX` z6H}5F6Z>fIXlHI|V+I357YmFPkm?cs&}T3sldtjp_~T|wHt&+S_y=qJ-%6CTDCN8$ zy?+SuB!BP-CA;d^*9VN}y85&=5j91y9$_3@98{cRab6bibb8(GSEAi+$=#qZ*~&&K z_@VGAwy6iEqNBSSed~<>u)06`BMpvn>{8PsOq{!5QW!vu`9~gBGII^abkWYjdL7I` z+~@DlM+*SX!G$vXb9nUfzzZw!*kq39`ME zwi65t3)R~R>z*&<`YJ?pmX;Ss+(SjdMy6M`X^wmq5j%@(Ig8l=0A{w%Fk+5oM$TrY zAKfgSe}0sdmRHjB!ytr#`3NKZT|~_te6s4R7jM@7a!$zUw6%iOgE{3#f@7H~$6ej? zH#@c2$`X=?{>5fyUg3b;YAi}w@=~fLu{nd^3|QN+!Ze~$UX(}Wne#`Zyti9@g{?<@)R08 z6h)%!MPQ_+rrw`mhNgm1X8JRA*JP?tCxU;lVF0rnP|#p9Q}?L& zbwn&el`3v@<$$iq<2?z7DSNH7E zbq00?vzR*4t2L9N^=1=w?6(mTRDzk6+C|)`vxZ$@qJr`ut19x6z%ne+&`jfKE-lPC zL$>wHdp07pv5T>vTp7c|<^r>ZxX~o=b?kDhwztLNZ=-2}#&%U@N62kvrgT)R)+|jx z+$^?@sfUMFo;Sx~b5;r9H;bkwxgy0vFtG9QgO+SCJON**so#l>u%XYZy0olb9WUXk ztLK{sVTtOgsj25%Ol16BJ zUaoOdoY#eCaRmTr11PmX4QOv`CtCNc-dY&!9Uzc>P>%Jg2aikjU;_Q$nns@H+$8=k zX0MYWO;!IA*di%;6OU)Sd%HUb!l?)Udew#Aa4LHiy()U|_p{$tJO^07!rFEHRWU8!z4pQ>0@!Z>y|}?Sw`aF436lm-q{BZPvVJN( z^JLVcP9^e(vp;yuwx}S*HoVS(s?)cOd9j{~53|_MKQ@DFgHv=;+Er`Fq$Bbnd%`Y% zxjuG`!WB)t=|t%4>BOOqIG4v^-Hc_3_;WVH>srKn-fRnXZGIx%q9DS2P++s~M>*Z& zd1m${9I!fC`ge%(+e@CBPateE^KQy@=!+U;xkFMHS90H)ar|{>1-%?%2DS;p_q3=^ zt+}{9N4bv-r3!_t{P1f5(@vaEa;Dm+k2ScKQ(Gvo?5v^Q)kB$S-4rkw-JWV)g$uXq zlSd6yDWPJbdRRuhNdu4yT1rpE@IuAC1mE7NJ&WwX=Q2!WuQk*DD+C)2z&=!9eC1JK zHq*o-guz-DSl4hd$z%JHIVI+TzwTp>+Ak@XuUjc>H>bITF4o$#Wc4gV+pCM*bO<~8 z@(k+|PLKn+!jsXOjI6PAz-VeoeVKP1`Cz_6H1n^WsQjBPF+B2*r|#k$=Mik2idvI< zY+FrMR%44sE|tvye)qhXpqKhoN~c;WK7+y#`H}b+6uMpnnL;awNOuVT=+mv9_=(WP z;IgHOAy=m`hh62~;+LW9s)Sejt2mB*<$N3OFb|9s8@y1w>^AV0Y z|0VNR7A+|W!YB?mPt3WF)6cCNaY$`TB!4>&9IQB@+uIALGe!0q!H0gayXDSB^_m_KCR%-T`-gIXcQsT1M>5DqBPmJ_OO zx2@`_BpIggsl4Mi@@J`i{2J4Pfp4Wo=O*Gs>|!7e05x}J+~!=YWG4>W(`Y5{CKsRM0mT z^wMcR&&(H=VRY9t(%*|tYVhIdU0bxVYm$JLQHtpXKmzQ3g7|jDaN)KWS-uyJrC519 zFptyKl_snmCvk7vB$+ogVubYfa@LBECi9;7T_eZ1XP};oM|XOj>}xQeGr}zsiuzM77V{)OyF*G zFxQPX8+3!JaPLR2_yV`wgX1s>Shh!CYlp}QMEYo(TCbIn734+gd5AdK1LBD~?_p65 zicPM5(z$!#LR?7u1ETXxIAy3qYh6Oe>?+JJ$A27u(-66WFb>MqIM^I<5HRTv=zBW# zwABvEg!eZ=Ve0!mxjWj4_7dQU1^ON4yGYVg`dSZ020ds(%rM7H`0ZjZM=@Tv(!lCd zPs?KwACJ=QM&-M$&|aGCpZ!-4_#nlIKH$Rj>;gqE+cnuNL~qU}J!WKcy%cDnTp)8i zx4>y+&%qrYb-DGKX_(Pe*ztWBK%l%ibcYr2y^T55qnQ1tL51m*b!ljNf_RF~I9St> zXOT6W2NSHky0guyEtkN`Jg7Zoe@d(?GM++IknV{)O+Vu0w*p0UfKZ&$D$f;Zy>NsZ z4EJ0}(cG8|)G~0l>HczEmD@#+6q)*=_Q4P2E*oM?9ZA_thp%G)Y9dT zDHHL-nsVKa%}nV6`u+_8DIthAeb{>rIwrf3tWgO_!y<|!a?xdCm*`yf{#(HRg5ZdW zhV&s|N_yjuIMWZ(fryCj@i&L7n&SnZ__S5`V$G)L3~E7rr3*8@61)usW*M@}4eIal z@miZxewWg6?m-kAjhbl7dn(I9|KbHdai?#);{$yK6<=QXxqo~Oh^^)|gEHr@_hJ={ zk%f(I=Qv**Cw{}9=2LT%_fAkeWnql7fJFa5IFUlo`8$2e?O%U=9;r)5$5L?kZ=)AR z&8Le{@+3kkQslvrhqb+u-RhA4{eTzUgzhM6B>_&7zz4?8sj+Pz4$vs#u2D2swiM{M z)5cRGI`s6D=V9BZSJ78)SvvO)8fZS5p1_g%^Puji)}5v+8c3o8SuxJ*h_d~8Ku6!_ znd;voSY*P<{VC|SBh>?wnQE`N*ydwOHs;vYsde|nh>_bxOeK#LCeBBknes;CZyNrY zM{JS&mnIyPB~7d6cNZ@}|KwWp_lapi+fYn?oVfUiF&rX-hMW4Cwi~)H?G25)4EGT= z%$LB$t#Uh21~pRy5{1*EO_y(XZ`Nnr*Y;%mruf z8RT!B;j7lk3Q=*D3E*LzE=mpg5YiFYoCEaO)dAE7#ETZ)C)Bqb%1*6AT&1@3dC?Ar z=$cCLQRy*SxaAf%ZEarnHl-35=;#AjR%T}|(rPD*Q8UZ2o|;t#LU1jgl_WOnfnmk2 zjJ?xb)st?Ao$ongNnmnII#lqJWigKwU2R3y-P3gCVR zZO6h(bGf#jzJ{ohZsidhyPEjc(Mi~T9SXXk+8-XwYa{gnY9v{_aA9%NsvMn~_BMvx0R?vsR736CQ zvFfwune|nT%ACnQfZP)3%-6E*07fPE936+ni1dLd`2z>p#*kY?%5m`gGHHX+%wM;v zomt?Q50mM5m1BkbskyVT`z&c|YbU40M<7(-i%teeeUiFXo_f~WJ_m!D>Ah?mfo2ZX z{@EjOW%yRgu-TOS8YqIGS(pFV*&|Ckz9>&_u)ppcDClD*=wUR3cJK0@>fs%x`ogK` z#e!X7_YN%lEZMx0aVm|H+a~YU)8x_S9WtR=HRSB{d$4oWY07Vkp}Jyryw=Qt z9L&Q|r@T0iaCk<5U9MMEL&G#e+y?w(EZTn^Gt^TAO57kZkl}zrIgb|>D%NI|4;tpA}shN%~H@&XNTl1L- zq!5h>!$Z=Ls_O%>%&TlYhp1et`sE~qU=IpULALD&HH;CT6tQ-5IrwSAB`^0HRVBIg z%14U2p`|-peUZDm?7+#)80}mK#bo)x(o1%6c-qGGrQ?23`uy&-Y8($*c)rJ^TAB86 ziJc0_6=I6h<2UTRD>U~kY0nf(5YH&V<^^8ow3s}_>~X&MX~>}@wslC$<;)9GlR(8T z2|fa0L@vm+u|ze?Y32B@Sbf`+S<0n<)&zLT4Z2w(!pqV;>eTW?XPfHcDVgEEE>3e?CXettJOxU~m+C z8!Td>dPzv~Faj_+`K;b>*JS}p|NKdmTLZHeNlh=F${Ka6`;iy#;NUMuE{zi5Z|BX? zLtk=guX`PqSHDGh_pTsfW>F(l{Fb=wh-+e9Tk;D{lKYBer*> zG{*PyO#MA4fooXz0VAcwF4;Fy>osSc%X0UL>1rwl$C!#lpR{n(d)kksHn>b-hnQ_!E57?3woL$ zt`^6B-Q3z%xFm9Sv4|$7D7MO|Q}mkEI2J1bg3Uj0V(tH8%kg|ma~nDHtdRq#9y+Wo z+7kV&ER;$_hrpP0rMB(`8sZ-LM`?#o-gV3{N!PSXD*gSKq~NM{fBDS#3|q0!i9{m~ zH^;U_msc9q^+k0X^)MN@15;|G($#)9jzD#};v?tPJZiBa2=_)AVk^l`P-gYQa&@zH zL9_n_75dTl-q^_>un^1@iJ67XIm;^n?QSrptnxoh>N7`GX$9H-YfJLfo39_TPrI8S z9*6Eh``!b0`+b^shb1jTBslU;!T}K~r#a<{xm37k+;8o9mp`R|6 zF#<31F6oIs-8cQGxF8Bsvji8=$KlIH6X}rG4wc}tH_A^~4~pe-ccv?V!&a7}9Bj?*i9qgb0s&mHM=yLI%pUg+&Zn?9>xCT8V=m({sD zzdJv<^N+&j<`n%l&!=Bwyi*pD{Xek6==UZ-1N!*RbPKnQ15?kJtoF+-fo3nF?Vd`` z^iLx@+pQKxU@GGDmsqUw(9h96{RuD0V`oIg)|7CE#e=?4W)J_^&ka9ppeS>T{U1 zFxz~iAEu6Ys;&5k%X8VT!{E6dA>L8#r(aqPB#a&>>WdnOlD5JXq7~D;ZbVzjN@WZe zpSM)vd!@DbDCO#ZbEFxyNk=Gm9_5r7QkhM;N=V9#p*rZ$HC)+{16th@68aS74LM_+ zAKY`8xotDrV^UdTa!+!|4=ta2GIRIZ!wP?*u0cz?e)dhaU?jrre~LQzwsON5aqeIB2ibAu&?1V>|eE7c@u!_YZ7+_W%Hj~94e-2UTR&T&5) zf$yVcJv^?qdeR#N-e$WCYrPMraBGwKZ}9(b&i}Efe&*nFE58$VYDqo=SlyueVj$B* zH9;*1YqQSp>t|IDUA$caAp^PQ^>8xhw9LKg%_rmb(&=>^#+xqOCJVJszgu^+N7y%0D)Vc$X6}KRZG0UjSE(WQ!*1NZ&<(lv z{)rLYBVLOE&)&;hNXX@*zny!NK3qL;Jlf+Vy=@ViF;>TjS4X9QkrollhR`WKwS2^5 z%#OV*Lqt$XPwjk$_D9T*w==#wPe{Js$VRJgQ31RDGhVCjFQccpFm~5Ib}gx63!VW0 z-J%_d$X%QVoO5Qjx$ZdrFLS$QyOMf~51g8w#1T8cMk;rpF*4IhC~e|O+v3pWTWiGLE|KdA2Au+fIiJ7wNUMoJs?*YKQU?QA{*B;O1$Z5%wE7^-Y^SdLEhobeGfK)d9r_4K`oyV`C0OLtU?&`xx zI2p{NqItY&TJy~+hSvyz;{_el#9aQ9IADwD6(MVuW!X2P3h?{+5yuVwM8e*q9nn_S z3ZBUqxoyvTam5J$pd62zjfXH$8INdnobW~Aia}!C*eyXPvqOQ_BMkG5R7A$QW8+yK zx^h#E$a(TMv22vg{TI+m44GTgX=w6y9aCi1y|Mv8#?&rlu2So6T>FR&VF@cV6hCf0 z`)ioGoX9uQgT*DrLy?AF`Pb*5*%3|Ey0IXWBI**XAEl(2Ps<69Bc}{GD#pZkmc78g zze5~vt1s9w(l~>HJ35i%r(E2+BIMmN>ts($}Z_XG6$fv$&sfH9%m+p zLEk6fhy3-OyDd8k#IR9gWn_gIo4MD)-d2C=qziDu)IumWqVrV^FaSy>W9UYcbap-J4`R&{_QlTV{^jKP2t-AB;3p) z>C>;&VCiD3IV06++L-T>8lHIWU8U^(XiQg~5KpKBACGMWY+G8ZCd#DUp!r%BQk0#0 zkT|0t4W$>ghAf=4=Kl8vZIHx}uIy5gImebFeGz1*_KvlbPG!$!U>lM7Yphn#J8n6j#>vPLC_PK|zh z68t=4a$bWf;rxc&hvxJ?J3!7${5$UUA2QR6$<&f1)Gw~@%vfh*&VSOlQe`E@E$aa5 z>L=RAT3cWx#@yjT#0S*15vGJ^IDfQ7wB{r1zp$oyEc6MBQ_AY=$@savKj7{>GCd-6 zF%@8o9x^BF8zHRme1cKw{|v`)!&tt3$|6Q_7=w*QIWATd)z;tp*UW&UnLEDNZ87#^;q%1$`45}FLjsEdY**mKNB`g z?wDVSDaIwC&UOXYOQXEx^y3>ZVa!j$v<&r?LNCJTT*Oo61QA zFSmH3nDx+p%Var`;d!m6du-|?>3~J3JI<@sZ)^F$*iP%K=Sy6{vg?>{YFG{DMTL#T zyhhc*Nj{T)4yRLddI~NIHn#lQ9Tn4ePiu#I4!y}5>6QWRWOLO*P6;KBK(2r4g1Ymk*%>P?otFC0dIX-% z$N~3JZX}R~E18e{SM)-K*%Za46j6K^*;m@HjFOdelPqD@j^!GZ95Uji6@I~AsF>x! zEoL7>=s_zkKlQ;K+)RPrECvo!uJpYNTkMxnI*ig>>1#PFXbLNWX(5maRWE<<0l@cn zn5#q+-&6gG*(B+drjhvwva#@qyZAVB6+@V4m&|QDMh|r+4vty`Uxco8>=vFM8th2} z?1;MweZeE-t0LQiBcdEPv{dJ{_M-!q2HP_8Rf* zz8bb4C%Mp{D4am5>|s1xiUvj+qbTH>fPtIZ_J~J+nSZ>-OYP>kVg=|Jyrqp}{}xwW zv1M#HsGu_DTI%#3vWd0Bydh=Qsr{4)4tCB>D`C!6O;L{0>iTp*0P`J7On!dK;!&FNsR|@YgJ9>b!azAH`V< z*5iJ6DwS#GT6J)qIhkQIzUWAa>n@av#W`G+8*hPeN)F*EH%iK~N(3jVF12u^s@~oB z?%fC!dKQ+~#w31;_V5Lb9c$Mn3s}=61J#dnYlqtV)@;T=i>Lb`rS|nJffQ%lOz1y$ zYrZta>&FfS^3kvb!fE(Sv)PxF1X?OESdnM|N(I4a#|#V%@YeLP=e^<#X%1Ck@KWpq zwLamv>7DQLqdRJ1903CgW_sfcS4Dp-?%kuYa(X;(f3I6Pebjo<_rNKqBwn$_JpIYJ z5DXWHMPa+XxWRifkLVeNi!)(+6R>33`2k!7>TE0gU0*=t_&yld3`P!RfhGuhAT&(F0r?qamzsBI! z93aO+{F!Qj_yiBBn_uN~+{)6#LI?|d(3<_JouB%+*h##DX@8_I>ZynusFK7lzv33S z7TQ^HB#~Km$l%TS=VV}r)sxb#GHK23@?~E&#GTD64A*siBU!kOuX@}-)LQ$i0zn?7 z@Q7LQrDod|`lB4l_Sisa<4c*8)2^M@_l+p=2BGxXizWy;ckub?OyekbtV!_{-o{5D zX;X}sj$t)UlHEu++=4F5bR|yVw1jZb1NyBfX@iI}NSSO{HL_+Eu}YsugoYYgIzQDShMek2Qec}aqm`Pb3>Hd8bmT1@$QgqqL8M_R)ZWw|BX5?WxF29*r2C9{Gm^1_rL>trlP)pyEhPQ*)+Nlhq@^ zm4~p;S6fOMLcHSpgz&74qlqn>!9=;U(Rpl1`F;5lfj4u)qr<~kbSP@Dbji9TjnB8G zT9&H-wW{b;k%qbktWCI20{;t<{vQy8^uG|Pw~vNfu08j1K)>=0&Ya`2y`muGIToau zrXEjc@XfZkdI7D_=> zL`g}>(aZSy;H)&W!c|wVGNbz+G^@L|;gSNq!L&W{lHhrbpU3?&MQ@Mq#`+5ygXdKm z9oUIX*Z#ahJy=6FA{}&fu@PJA*IYd^a+eKvu4T$>-WxdlQ(*a;`8Qu$bi`Z0Vv^Dg zE?KhKoy-=)DS5SrWtdICc^}KX_CA6Q(D3H5iM<}^?bhwX`Mvj@w_vM2wD`?~t}Tkp zuibn5x^1{Kb)bM+gJZ<_a1kyO!Ni)0zRZ7wxYmotw-%UI1#t zB+!kPh|(e{!CZ2r3+xEX_FKkWB&knp|5LJ12&eT{oq#3Qu;ZOmkWF$-QbMmK`gQ#H z`rdmiWB>MH0!bD5zd8%!=r49gD`*42y126G9gK6@YX zJO``U5dV?ysok08ko&Clrj!x^Ybe&wvAUgomF_Xj26N~IAQZh};ZRg&C0*3H#16aG zFZJHWTUd5gqIsIHe%UmJmN)zZ2}yA@%)uvo{I664(Yos41u?3f15PKk9{5`K0wXQ1 L@V!FR(EtAcu$6yT literal 0 HcmV?d00001 diff --git a/vscode-lean4/src/utils/leanInstaller.ts b/vscode-lean4/src/utils/leanInstaller.ts index 446194472..2452efb5e 100644 --- a/vscode-lean4/src/utils/leanInstaller.ts +++ b/vscode-lean4/src/utils/leanInstaller.ts @@ -147,7 +147,7 @@ export class LeanInstaller { // note; we keep the LeanClient alive so that it can be restarted if the // user changes the Lean: Executable Path. - const installItem = 'Install Lean using Elan'; + const installItem = 'Install Lean'; let prompt = 'Failed to start \'lean\' language server' if (path){ prompt += ` from ${path}`