8000 Make BackendName a Text by andreasabel · Pull Request #7479 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Make BackendName a Text #7479

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.

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

Merged
merged 2 commits into from
Sep 9, 2024
Merged

Make BackendName a Text #7479

merged 2 commits into from
Sep 9, 2024

Conversation

andreasabel
Copy link
Member
@andreasabel andreasabel commented Sep 9, 2024

Main motivation for this refactoring was to consistently enforce the type synonym BackendName; so I changed it from String to Text.
In the long run, we should deprecate String for Text everywhere, but this will be another mammut refactoring.
Also changed the "installed backends" list into a bullet list in the error for non-existing backend.

andreasabel added 2 commi 8000 ts September 9, 2024 17:56
Main motivation for this refactoring was to consistently enforce the
type synonym `BackendName`; so I changed it from `String` to `Text`.

In the long run, we should deprecate `String` for `Text` everywhere,
but this will be another mammut refactoring.

Also changed the "installed backends" list into a bullet list in the
error for non-existing backend.
@andreasabel andreasabel changed the title backend name Make BackendName a Text Sep 9, 2024
@andreasabel andreasabel added refactor Changes to the code base which do not affect users (not in changelog) backends labels Sep 9, 2024
@andreasabel andreasabel added this to the 2.8.0 milestone Sep 9, 2024
@andreasabel andreasabel self-assigned this Sep 9, 2024
@andreasabel andreasabel merged commit cfaf03f into master Sep 9, 2024
28 checks passed
@andreasabel andreasabel deleted the backend-name branch September 9, 2024 19:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
backends refactor Changes to the code base which do not affect users (not in changelog)
Projects
None yet
3DF2
Development

Successfully merging this pull request may close these issues.

1 participant
0