<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>I don't see the Agda menu in Emacs <br>
    </p>
    <div style="font-family:arial,helvetica,sans-serif;font-size:small"
      class="gmail_default"> After running</div>
    <div style="font-family:arial,helvetica,sans-serif;font-size:small"
      class="gmail_default"><br>
    </div>
    <div style="font-family:arial,helvetica,sans-serif;font-size:small"
      class="gmail_default">$ sudo apt-get install agda-mode</div>
    <div style="font-family:arial,helvetica,sans-serif;font-size:small"
      class="gmail_default">$ emacs Foo.agda</div>
    <p>But I have ALSO installed the agda package and now I see the
      emacs mode Agda.</p>
    <div class="moz-cite-prefix">Le 18/03/2020 à 18:24, Andrés
      Sicard-Ramírez a écrit :<br>
    </div>
    <blockquote type="cite"
cite="mid:CAOUWSGCpMwZwi1HahUFojTLs1qa6yjcXZ7zUG7bOxnZcKwNxSA@mail.gmail.com">
      <meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
      <div dir="ltr">
        <div dir="ltr">
          <div class="gmail_default"
            style="font-family:arial,helvetica,sans-serif;font-size:small"><br>
          </div>
        </div>
        <br>
        <div class="gmail_quote">
          <div dir="ltr" class="gmail_attr">On Wed, 18 Mar 2020 at
            11:08, Michel Levy <<a
              href="mailto:michel.levy.imag@free.fr"
              moz-do-not-send="true">michel.levy.imag@free.fr</a>>
            wrote:<br>
          </div>
          <div> </div>
          <blockquote class="gmail_quote" style="margin:0px 0px 0px
            0.8ex;border-left:1px solid
            rgb(204,204,204);padding-left:1ex">
            <div>The output of <br>
              <div
                style="font-family:arial,helvetica,sans-serif;font-size:small">
                $ sudo apt-get install agda-bin</div>
              <div
                style="font-family:arial,helvetica,sans-serif;font-size:small">
                $ agda --version</div>
              <p>is <br>
              </p>
              <p>michel@M1330:~$ agda --version<br>
                Agda version 2.5.3</p>
            </div>
          </blockquote>
        </div>
        <div class="gmail_quote">
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default">Ok.</div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default"><br>
          </div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default"> After running</div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default"><br>
          </div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default">$ sudo apt-get install agda-mode</div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default">$ emacs Foo.agda</div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default"><br>
          </div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default">Did you see the Agda menu in Emacs?</div>
          <div
            style="font-family:arial,helvetica,sans-serif;font-size:small"
            class="gmail_default"><br>
          </div>
          -- <br>
        </div>
        <div dir="ltr" class="gmail_signature">Andrés</div>
      </div>
    </blockquote>
    <div class="moz-signature">-- <br>
      courriel : <a class="moz-txt-link-abbreviated" href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a> <br>
      mobile : 06 59 13 42 53<br>
      web : michel.levy.imag.free.fr
    </div>
  </body>
</html>