coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] external editor in coqide

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] external editor in coqide
Date: Tue, 29 Jan 2019 03:21:16 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:PcJxrxC3om2SUYUK9N4oUyQJP3N1i/DPJgcQr6AfoPdwSPT8pcbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCupx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9zrzS1wsohiZHFip8Vx1zY7yl13po5KNOiREJlfNKoDIFcuzyUOoZyWs8iTX9ntSUmxrADvJO2eCsHx48oyhPadvCKfZaH7Q/mWeafPzh1h25pdbehixmp/0itxevxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw81uv1jiSywzf9/hIL102mqfVMpIhxaU/mYQJvUTEAy/2hF75jKiLdkUi5+ek8fznYq/hpp+AKYB7lh3+MqUpmsy5G+g4NRUOX3Sf+eS7073j/lf1T6lNjv0ziqXZsZbaKtoHpqOhDAJZzpwv5wujAzqkytgUgHcKIVBfdB+DjIXlI1TOL+r5Dfe7jVSsijBrx/XeM7PlHJrNNGbMkLLhfLpn5UBT0gQyzctY55JSEbwOOvTzWlLruNPGExA5Lha4zPz6CNllzIMRRXqPArOFMKPVqVKH+uUvI/CVaIAJvDb9NuMq6uX1jX45nF8dZbOm0YEWaHC+BPRmIl+WbWDigtcbQi82uV90R+vzzVaGTDR7ZnCoXqt66CtxQNatCp6GTYSwipSA2j26F9tYfDYVJEqLFCLKep+JXuZERCuNOchn2mgmWKKsTp5n+Rixrwj847NhM6zZ9jBevI+1h4s93PHaiRxnrW88NM+ayWzYFzglzFNNfCc/2eVEmWI4z16C1aZihPkBT45a4e4PXwsnc5fBnbUjV4LCHznZd9LMc26IB828CGhrHNs33pkDb1s7Esjw1kmejRrvOKcckvmwPLJx8q/Y2CSude9A8C6fkZIQ1BwhSMYJMnC6jKli8QSVH5TOj0iSi6etc+IbwTLJ82CAi2GJuRMBXQ==

Hi Laurent,

I tried this, and it said /bin/sh: 1: gex: not found

Is it in fact the name of the editor that should go here?
Is gex another (similar?) editor?

So I tried putting vi here, and I got
Vim: Warning: Output is not to a terminal

What should I try next?

Cheers,

Jeremy

On 24/1/19 8:45 pm, Laurent Thery wrote:
>
>
> On 1/24/19 6:44 AM, Jeremy Dawson wrote:
>> So how do I start up my usual text editor (vi) while using coqide?
>
> You can configurate the editor in Edit->Preferences->Externals->External
> Editor replacing emacs by gex
>
> --
> Laurent
>

[Coq-Club] external editor in coqide, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] external editor in coqide, Laurent Thery, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Théo Zimmermann, 01/24/2019
    - Re: [Coq-Club] external editor in coqide, Anders Lundstedt, 01/24/2019
  - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019
    - Re: [Coq-Club] external editor in coqide, Jason -Zhong Sheng- Hu, 01/29/2019
      - Re: [Coq-Club] external editor in coqide, Jeremy Dawson, 01/29/2019