<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>