[Agda] help with math symbols
Serge D. Mechveliani
mechvel at botik.ru
Sat Aug 4 10:17:03 CEST 2012
On Thu, Aug 02, 2012 at 04:15:26PM +0400, Serge D. Mechveliani wrote:
> On Thu, Aug 02, 2012 at 10:38:28AM +0200, Dominique Devriese wrote:
> > Serge,
> >
> > 2012/8/2 Serge D. Mechveliani <mechvel at botik.ru>:
> > >> > Thanks to my colleage, he noticed that the expression
> > >> > (shell-command-to-string "agda-mode locate")
> > >> > evaluates to "/home/mechvel/stdin".
> > >> > And it is natural to suppose that in my installation case this value
> > >> > rather should be
> > >> > "/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el".
> > >> > Right?
> > >>
[..]
>> -- citation -----------
>> bash -c "agda-mode locate" | less
>> /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
>> (END) > -----------------------
Guillaume Brunerie <guillaume.brunerie at gmail.com> asks
(on 03 Aug 2012)
> And what's the output of
>
> sh -c "agda-mode locate"
The same:
/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
-- without Newline in the end.
------
Sergei
More information about the Agda
mailing list