Labels Milestones

Add scritti_ro.sh and reformat readme. #4

Open

alberto wants to merge 2 commits from alberto/dm-scripts:main into main

pull from: alberto/dm-scripts:main

merge into: phc:main

phc:main

phc:removeproofs

Conversation 0 Commits 2 Files Changed 2

alberto commented 6 days ago

There is no content yet.

alberto added 1 commit 6 days ago

66b1485213 Add scritti_ro.sh and reformat readme.

alberto added 1 commit 6 days ago

f24b3d7f8a Merge branch 'main' into main

This pull request can be merged automatically.

You are not authorized to merge this pull request.

You can also view command line instructions.

Step 1:

From your project repository, check out a new branch and test the changes.

git checkout -b alberto-main main

git pull main

Step 2:

Merge the changes and update on Gitea.

git checkout main

git merge --no-ff alberto-main

git push origin main

Sign in to join this conversation.

Reviewers

Request review

No reviewers

Labels

Apply labels

Clear labels

No items

No Label

Milestone

Set milestone

Clear milestone

No items

No Milestone

Projects

Set Project

Clear projects

No project

Assignees

Assign users

Clear assignees

No Assignees

1 Participants

Notifications

Subscribe

Due Date

The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: phc/dm-scripts#4

Write Preview

Loading…

Cancel

Save

There is no content yet.