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.

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

Exercise Development Mode: Title Editor #928

Closed
wants to merge 9 commits into from
Closed

Conversation

LutSa
Copy link
Member

@LutSa LutSa commented Nov 8, 2022

Add Haz3l title edit.

Copy link
Member

@cyrus- cyrus- left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good, but see small comments.

You also need to update INSTRUCTORS.md with updated instructions, esp re:prompt.

@@ -36,6 +36,9 @@ let is_action_logged: Update.t => bool =
| ResetSlide
| ToggleMode
| SwitchSlide(_)
| SwitchTextEditor
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should we unify this with SwitchEditor since the focus can only be in one place at a time?

@@ -36,6 +36,9 @@ let is_action_logged: Update.t => bool =
| ResetSlide
| ToggleMode
| SwitchSlide(_)
| SwitchTextEditor
| UpdateTitle(_)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Let's group all Exercise related actions into an ExerciseAction.t type that is injected into Action.t at once, to avoid having too many cases?

@cyrus- cyrus- marked this pull request as draft November 21, 2022 02:53
@cyrus- cyrus- added the needs-polish for PRs that are substantially complete but need final polish label Nov 21, 2022
@cyrus- cyrus- changed the title Add Haz3l title edit Exercise Development Mode: Title Editor Nov 23, 2022
@cyrus- cyrus- changed the base branch from haz3l-tests to dev January 19, 2023 19:50
@cyrus- cyrus- added needs-merge for PRs that need a merge from dev and removed needs-polish for PRs that are substantially complete but need final polish labels Dec 11, 2023
@russell-rozenbaum russell-rozenbaum marked this pull request as ready for review May 29, 2024 17:40
@cyrus- cyrus- marked this pull request as draft June 7, 2024 01:26
@cyrus-
Copy link
Member

cyrus- commented Jul 25, 2024

closing in favor of #1316

@cyrus- cyrus- closed this Jul 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
needs-merge for PRs that need a merge from dev
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants