<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
<div dir="ltr">Aha! I wondered how to check what path Emacs is using. Answer below. Thank you for your help! Go well, -- P
<div><br>
<div><br>
</div>
<div>exec-path is a variable defined in ‘C source code’.<br>
Its value is<br>
("/Users/wadler/.elan/bin" "/usr/local/bin" "/usr/bin" "/bin" "/usr/sbin" "/sbin" "/Library/TeX/texbin" "/usr/local/go/bin" "/usr/local/MacGPG2/bin" "/Library/Apple/usr/bin" "/usr/bin" "/bin" "/usr/sbin" "/sbin" "/Applications/Aquamacs.app/Contents/MacOS/libexec"
"/Applications/Aquamacs.app/Contents/MacOS/bin" "/usr/texbin" "/usr/local/texlive/2022/bin" "/usr/local/texlive/2021/bin" "/usr/local/texlive/2019/bin" "/usr/local/texlive/2008/bin")<br>
<br>
Original value was <br>
("/Users/wadler/.elan/bin" "/usr/local/bin" "/usr/bin" "/bin" "/usr/sbin" "/sbin" "/Library/TeX/texbin" "/usr/local/go/bin" "/usr/local/MacGPG2/bin" "/Library/Apple/usr/bin" "/usr/bin" "/bin" "/usr/sbin" "/sbin" "/usr/texbin" "/Library/TeX/texbin" "/usr/local/texlive/2022/bin"
"/usr/local/texlive/2021/bin" "/usr/local/texlive/2019/bin" "/usr/local/texlive/2008/bin" "/Applications/Aquamacs.app/Contents/MacOS/libexec")<br>
<br>
<br>
This variable may be risky if used as a file-local variable.<br>
<br>
Documentation:<br>
List of directories to search programs to run in subprocesses.<br>
Each element is a string (directory name) or nil (try default directory).<br>
<br>
By default the last element of this list is ‘exec-directory’. The<br>
last element is not always used, for example in shell completion<br>
(‘shell-dynamic-complete-command’).<br>
<br>
You can customize this variable.<br>
<div>
<div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr">
<div>
<div dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr"><br>
</div>
<div dir="ltr"><br>
</div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
<div dir="ltr"><br>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
</div>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Tue, 28 Jun 2022 at 16:38, Nils Anders Danielsson <<a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
On 2022-06-28 17:20, Philip Wadler wrote:<br>
> Thanks! I tried what you suggested, but am still getting the same<br>
> error message.<br>
><br>
> Could not find agda-mode-2.6.2.2<br>
><br>
> Listing from the call to cabal appears below, for completeness, along<br>
> with my current $PATH.<br>
<br>
Please also check what the value of the Emacs variable exec-path is:<br>
<br>
C-h v exec-path RET<br>
<br>
--<br>
/NAD<br>
</blockquote>
</div>
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. Is e buidheann carthannais a th’ ann an Oilthigh Dhùn Èideann, clàraichte an Alba, àireamh clàraidh SC005336.
</body>
</html>