Repository navigation
Conversation
rfindler
force-pushed
the
avoid-drscheme-toolbar-buttons
branch
from
October 7, 2026 20:11
81ca785 to
229c190
Compare
Member
Author
|
@mikesperber we'll also want to change Deinprogramm as I'm hoping to disable the |
rfindler
force-pushed
the
avoid-drscheme-toolbar-buttons
branch
from
October 15, 2026 20:57
229c190 to
3c4da84
Compare
instead of drracket:toolbar-buttons the later is just a set of symbols that the language offers to drracket and the former is an arbitrary callback (that gets run as a part of drracket itself)
rfindler
force-pushed
the
avoid-drscheme-toolbar-buttons
branch
from
October 15, 2026 20:59
3c4da84 to
23e2841
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is part of a larger change to avoid using
drracket:toolbar-buttons. The power that offers is not needed here because the teaching languages already are using the drracket plugin API.@jbclements @mikesperber I've tested this trying out the
#lang-based teaching languages (which is all this affects) but I would love to get some sanity checking here or maybe a pointer to a test suite.