Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Docstring error with Emacs 29+ due to changed escape rules for single quote #6714

Closed
WtzLAS opened this issue Jul 4, 2023 · 1 comment · Fixed by #6735
Closed

Docstring error with Emacs 29+ due to changed escape rules for single quote #6714

WtzLAS opened this issue Jul 4, 2023 · 1 comment · Fixed by #6735
Milestone
2.6.4

Comments

@WtzLAS
Copy link

WtzLAS commented Jul 4, 2023 

In toplevel form:
<UNRELATED>/9.2.8/share/aarch64-osx-ghc-9.2.8/Agda-2.6.4/emacs-mode/agda2-mode.el:217:2: Error: defconst `agda2-command-table' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
Unable to compile the following Emacs Lisp files:
  <UNRELATED>/9.2.8/share/aarch64-osx-ghc-9.2.8/Agda-2.6.4/emacs-mode/agda2-mode.el

Seems related to docstring single quote escape changes in Emacs 29+ (link)
@andreasabel
Copy link
Member

andreasabel commented Jul 21, 2023 •
edited
Loading

agda/src/data/emacs-mode/agda2-mode.el

Lines 264 to 265 in 09b63b1

list which should contain 'local if the command should exist in
the goal menu and 'global if the command should exist in the main

plt-amy added a commit that referenced this issue Jul 21, 2023
@plt-amy
Fix backslash escaping for Emacs 29
3c243a9 
Fix #6714.
@plt-amy plt-amy mentioned this issue Jul 21, 2023
Merged
@plt-amy plt-amy added this to the 2.6.4 milestone Jul 21, 2023
plt-amy added a commit that referenced this issue Jul 21, 2023
@plt-amy
Fix backslash escaping for Emacs 29 (#6735)
a8e3b83 
Fix #6714.
@andreasabel andreasabel mentioned this issue Jul 22, 2023
Closed
5 tasks
@andreasabel andreasabel changed the title Compiling Agda HEAD with Emacs 29+ reports docstring error Docstring error with Emacs 29+ due to changed escape rules for single quote Sep 13, 2023
@csams csams mentioned this issue Jan 24, 2024
Open
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
@plt-amy @JobPetrovcic
Fix backslash escaping for Emacs 29 (agda#6735)
ccf2eca 
Fix agda#6714.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
2.6.4
Development

Successfully merging a pull request may close this issue.

Fix backslash escaping for Emacs 29 agda/agda
3 participants
@andreasabel @WtzLAS @plt-amy