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

"The module was successfully compiled" should mention with which backend #5532

Closed
andreasabel opened this issue Aug 25, 2021 · 0 comments · Fixed by #5533
Closed

"The module was successfully compiled" should mention with which backend #5532

andreasabel opened this issue Aug 25, 2021 · 0 comments · Fixed by #5533
Assignees
@andreasabel
Labels
backends ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Milestone
2.6.2.1

Comments

@andreasabel
Copy link
Member

"The module was successfully compiled" should mention with which backend

agda/src/full/Agda/Interaction/EmacsTop.hs

Line 116 in dd552b0

"The module was successfully compiled.\n"

@andreasabel andreasabel added ux: interaction Issues to do with interactive development (holes, case splitting, etc) backends labels Aug 25, 2021
andreasabel added a commit that referenced this issue Aug 25, 2021
@andreasabel
[ fix #5532 ] CompilationOK now reports backend which was run
ab5c1d7
@andreasabel andreasabel mentioned this issue Aug 25, 2021
Merged
@andreasabel andreasabel added this to the 2.6.2.1 milestone Aug 25, 2021
@andreasabel andreasabel self-assigned this Aug 25, 2021
andreasabel added a commit that referenced this issue Aug 25, 2021
@andreasabel
[ fix #5532 ] CompilationOK now reports backend which was run
2bab72d
@andreasabel andreasabel mentioned this issue Aug 30, 2021
Merged
andreasabel added a commit that referenced this issue Nov 17, 2021
@andreasabel
[ fix #5532 ] CompilationOK now reports backend which was run
371cc16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
backends ux: interaction Issues to do with interactive development (holes, case splitting, etc)
Projects
None yet
Milestone
2.6.2.1
Development

Successfully merging a pull request may close this issue.

[ fix #5532 ] CompilationOK now reports backend which was run agda/agda
1 participant
@andreasabel