search

martinescardo / HoTT-UF-Agda-Lecture-Notes

Lecture notes on univalent foundations of mathematics with Agda
GNU General Public License v3.0
218 stars 18 forks source link

suggestion for users who have an older version of agda already installed #10

Closed williamdemeo closed 5 years ago

williamdemeo commented 5 years ago

Carry out the installation instructions, but instead of

echo 'PATH=$PATH:~/mgs-2019/agda/.cabal-sandbox/bin/ emacs --no-init-file --load ~/mgs-2019/.emacs' >> mgs-emacs

try this:

echo 'PATH=~/mgs-2019/agda/.cabal-sandbox/bin/:$PATH emacs --no-init-file --load ~/mgs-2019/.emacs' >> mgs-emacs

Then, when you launch mgs-emacs and load a .agda file, you shouldn't get a version conflict between your old agda version (2.5.*) and the new version (2.6) of agda-mode that mgs-emacs is using.

tomdjong commented 5 years ago

Very nice, thank you! I will update INSTALL.md