Skip to content

Alr.Commands.Edit: user choice for multiple editors#1577

Merged
mosteo merged 1 commit into
masterfrom
alr_edit_choice
Feb 23, 2024
Merged

Alr.Commands.Edit: user choice for multiple editors#1577
mosteo merged 1 commit into
masterfrom
alr_edit_choice

Conversation

@Fabien-Chouteau

Copy link
Copy Markdown
Member

Part of #1137.

Comment thread src/alr/alr-commands-edit.ads Outdated
@mosteo mosteo merged commit 601567e into master Feb 23, 2024
@mosteo mosteo deleted the alr_edit_choice branch February 23, 2024 10:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants