Mark/handouts
1
1
Fork 0
Code Pull Requests 3 Actions Packages Releases Activity

edits #31

Open
Mark wants to merge 3 commits from edits into main
pull from: edits
merge into: Mark:main
Conversation 0 Commits 3 Files Changed 6 +275 -54
Mark commented 2026-03-04 18:13:12 -08:00
Owner
Copy Link
No description provided.
Mark added 3 commits 2026-03-04 18:13:12 -08:00
De Bruijn edits 53c3e1859b
The Painting edits 1a5aafb19b
Retrograde edits
All checks were successful
CI / Typst formatting (pull_request) Successful in 55s
Details
CI / Typos (pull_request) Successful in 1m3s
Details
CI / Build (pull_request) Successful in 4m44s
Details
b9f378ab76
All checks were successful
CI / Typst formatting (pull_request) Successful in 55s
Required
Details
CI / Typos (pull_request) Successful in 1m3s
Required
Details
CI / Build (pull_request) Successful in 4m44s
Required
Details
This pull request can be merged automatically.
You are not authorized to merge this pull request.
View command line instructions

Checkout

From your project repository, check out a new branch and test the changes.
git fetch -u origin edits:edits
git checkout edits
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
No items
No Label
Milestone
No items
No Milestone
Assignees
Clear assignees
Mark
No Assignees
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: Mark/handouts#31
Delete Branch "edits"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?