From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from eggs.gnu.org ([2001:470:142:3::10]:50172) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1iouGp-0001pg-Ob for guix-patches@gnu.org; Tue, 07 Jan 2020 14:12:04 -0500 Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1iouGo-0002Yp-Pv for guix-patches@gnu.org; Tue, 07 Jan 2020 14:12:03 -0500 Received: from debbugs.gnu.org ([209.51.188.43]:43385) by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.71) (envelope-from ) id 1iouGo-0002YV-MN for guix-patches@gnu.org; Tue, 07 Jan 2020 14:12:02 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1iouGo-0002qV-Ho for guix-patches@gnu.org; Tue, 07 Jan 2020 14:12:02 -0500 Subject: [bug#39020] Lean won't work with the emacs mode Resent-Message-ID: From: Brett Gilio References: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> Date: Tue, 07 Jan 2020 13:11:56 -0600 In-Reply-To: <6436926df827431b44eff1c34acd96c38eb6ea0a.camel@logicandtypes.org> (Arvid Marx's message of "Tue, 07 Jan 2020 19:53:49 +0100") Message-ID: <87zhezqdxf.fsf@gnu.org> MIME-Version: 1.0 Content-Type: text/plain List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+kyle=kyleam.com@gnu.org Sender: "Guix-patches" To: Arvid Marx Cc: 39020@debbugs.gnu.org, bandali@gnu.org Arvid Marx writes: > The emacs mode for Lean (which doesn't appear to be packaged yet, but > of course works via MELPA etc.) expects some sort of root directory for > Lean, which is not given simply because binaries and other files are > put into separate directories. This of course makes Lean impossible to > use as intended. However, I'm not quite sure how this would be fixed in > practice, as I'm not aware of any suitable directory hierarchy in such > a case. > > Any ideas? > > -- > > Arvid Cc'ing Amin Bandali, who took care of packaging Lean. I am happy to help too, but I want to see what he says first. -- Brett M. Gilio GNU Guix, Contributor | GNU Project, Webmaster [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]