[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