From 9af2830371d72a9f2c1ee4898edb67db9d2d315a Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 11 Dec 2024 15:47:53 +0000 Subject: [PATCH 1/5] update pretext --- .devcontainer.json | 4 ++-- .github/workflows/pretext-cli.yml | 15 ++++++++++++++- requirements.txt | 2 +- 3 files changed, 17 insertions(+), 4 deletions(-) diff --git a/.devcontainer.json b/.devcontainer.json index 732ab66..7da7a9c 100644 --- a/.devcontainer.json +++ b/.devcontainer.json @@ -15,9 +15,9 @@ "name": "PreTeXt-Codespaces", // This Docker image includes some LaTeX support, but is still not to large. Note that if you keep your codespace running, it will use up your GitHub free storage quota. Additional options are listed below. - "image": "oscarlevin/pretext:small", + // "image": "oscarlevin/pretext:small", // If you need to generate more complicated assets (such as sageplots) or use additional fonts when building to PDF, comment out the above line and uncomment the following line. - // "image": "oscarlevin/pretext:full", + "image": "oscarlevin/pretext:full", // If you only intend to build for web and don't have any latex-image generated assets, you can use a smaller image: // "image": "oscarlevin/pretext:lite", diff --git a/.github/workflows/pretext-cli.yml b/.github/workflows/pretext-cli.yml index 22b8a3c..2be6660 100644 --- a/.github/workflows/pretext-cli.yml +++ b/.github/workflows/pretext-cli.yml @@ -24,8 +24,21 @@ jobs: - name: install deps run: pip install -r requirements.txt + - name: install local ptx files + run: pretext --version + - name: build deploy targets - run: pretext build --deploys + run: | + version="$(pretext --version)" + major="$(echo $version | cut -d '.' -f 1)" + minor="$(echo $version | cut -d '.' -f 2)" + if [ "$major" -ge 2 -a "$minor" -ge 5 ]; then + echo "PreTeXt version is 2.5 or greater; using new build command" + pretext build --deploys + else + echo "PreTeXt version is less than 2.5, using old build command" + pretext build + fi - name: stage deployment run: pretext deploy --stage-only diff --git a/requirements.txt b/requirements.txt index 17aca4d..745d844 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,2 @@ # -pretext == 2.6.0 +pretext == 2.10.1 From fec9e86e327d66c2efb0d12675cd3daa54119fb7 Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 11 Dec 2024 15:57:24 +0000 Subject: [PATCH 2/5] remove liveshare section --- source/ch-collaboration.ptx | 56 ++++++------------------------------- 1 file changed, 9 insertions(+), 47 deletions(-) diff --git a/source/ch-collaboration.ptx b/source/ch-collaboration.ptx index 97503f0..5ee20c2 100644 --- a/source/ch-collaboration.ptx +++ b/source/ch-collaboration.ptx @@ -1,52 +1,11 @@ Collaborating with Others -
- Live Share -

-A nice feature of collaborative authoring tools such -as Google Docs and Overleaf is the ability for several -collaborators to edit the same file synchronously, with -a feature set similar to GitHub.dev. -

-

-Using the Extensions sidebar, search for and install -Microsoft's Live Share extension. Once installed, -you will have a Live Share option in your -bottom toolar. Clicking it will automatically copy a URL -ending in -https://.../join?[randomStringOfCharacters]. -If you share this URL with a colleague (or -colleagues) you trust, they will be able to collaboratively -edit your repository's text files with you via their web -browser. When you commit your -changes, they will be listed as co-authors of the commit. -

- -

-As of writing, my experience with LiveShare has been hit-or-miss, -so I'll suggest another mechanism for live collaboration. -Sometimes when I'm working on a Git repository -with a collague on Zoom, I'll share my screen and give my collaborator -control of my mouse and keyboard, or vice versa. Obviously -you should only do this with a collaborator you trust, but it's -a simple solution to quickly work together on the same repo! -

- -
Collaborators and Pull Requests

-A particular downside of Live Share () -is that it requires -the repository owner to create the Codespace and provision -the Live Share session. As a result, there's no way for a -collaborator to make a contribution via Live Share to a GitHub project -without the active involvement of the repository owner. -

-

-To address this, one solution is for the repository owner to -add other GitHub users as collaborators. +A direct way to allow multiple people you trust to work on the +same repository is to add these GitHub users as collaborators.

@@ -89,16 +48,19 @@ must name their distinct branches.

-One workflow to support multiple collaborators on the same +Our recommendation to support multiple collaborators on the same repository is to never directly commit to the main branch, even if you're the owner.

To commit to an alternative branch in GitHub.dev or Codespaces, select main in the bottom toolbar, then type the name of your new branch, -and select Create new branch. The name of this branch could -be topical, e.g. add-derivative-chapter, but it's also fine to -pick some other unique identifier, e.g. lastname-YYYY-MM-DD. +and select Create new branch. It's a good idea to name your +branch in the form UserName/short-description-of-topic, +or if you're unsure of the topic, you can just use the current +date: UserName/YYYYMMDD. Note that prefixing with your +UserName helps prevent two people from accidentally using the same +branch name.

From bb6b1c5b8d29f0c0167606bfa6be37289590e7d8 Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 11 Dec 2024 16:05:58 +0000 Subject: [PATCH 3/5] accidental commits to main --- source/ch-collaboration.ptx | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/source/ch-collaboration.ptx b/source/ch-collaboration.ptx index 5ee20c2..40a0e2d 100644 --- a/source/ch-collaboration.ptx +++ b/source/ch-collaboration.ptx @@ -165,8 +165,11 @@ using main as your Branch name pattern, and enabling required pull requests.

+
+
+ Undoing accidental commmits to <c>main</c>

-Finally, there's no button to push that will fix a commit +Unfortunately, there's no button to push that will fix a commit made to the local copy of main accidentally, but there is a quick-enough fix nonetheless.

@@ -179,7 +182,9 @@ tthe error message Can't push refs to remote. Try running "Pull" first to integrate your changes.

-To fix this, open the Terminal and type , +To fix this, open a Terminal +() +and type , changing my-new-branch to the branch name you want to create. Use Enter to execute the command.

From b29fcad5c22c242ee45035560798a9cf78913efc Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 11 Dec 2024 16:09:08 +0000 Subject: [PATCH 4/5] warn branch issue must be resolved in a Codespace --- source/ch-collaboration.ptx | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/source/ch-collaboration.ptx b/source/ch-collaboration.ptx index 40a0e2d..70e6339 100644 --- a/source/ch-collaboration.ptx +++ b/source/ch-collaboration.ptx @@ -173,12 +173,18 @@ Unfortunately, there's no button to push that will fix a commit made to the local copy of main accidentally, but there is a quick-enough fix nonetheless.

+ +

+ This fix must be done in a Codespace, + not GitHub.dev. +

+

With branch protection enabled, if you accidentally make updates directly to your personal main branch, attempting to push these from a Codespace will result in -tthe error message Can't push refs to remote. +the error message Can't push refs to remote. Try running "Pull" first to integrate your changes.

@@ -235,7 +241,7 @@ shared branches.

Managing contributions from forked repositories is done using the -same workflow as I recomend for collaborating with trusted colleagues +same workflow as we recommend for collaborating with trusted colleagues that you've given write access to your repository (). The only difference is that an outside collaborator is creating branches and making commits From c33e8c86978b45e9b3876520678c491388b53675 Mon Sep 17 00:00:00 2001 From: Steven Clontz Date: Wed, 11 Dec 2024 16:41:02 +0000 Subject: [PATCH 5/5] add merge conflict section --- source/ch-collaboration.ptx | 61 ++++++++++++++++++++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/source/ch-collaboration.ptx b/source/ch-collaboration.ptx index 70e6339..dbf5e2b 100644 --- a/source/ch-collaboration.ptx +++ b/source/ch-collaboration.ptx @@ -273,7 +273,66 @@ and open a pull request.

Handling Merge Conflicts

-To come in a future revision of this handbook... +Perhaps the most complicated scenario when collaborating +on a Git repository is the dreaded merge conflict. +

+ + +

+While Git is fairly good about merging together changes +made by different contributors to different +files within a project into a cohesive whole, a +merge conflict can occur when two different +contributors attempt to make changes to the same file +(particularly, the same line) at the same time. When the +second contributor opens a pull request, GitHub will warn +about this conflict. +

+ + +

+Handling merge conflicts can be tricky! +Git/GitHub have various tools to help you review and correct +a merge conflict. If you're fortunate, you'll be able to resolve +things on the pull request page: see + +Resolving a merge conflict on GitHub + for full details. +

+

+You'll be presented with files with some strange markers as in +. The lines between +<<<<<<< HEAD and +======= were merged first, and the lines between +======= and +>>>>>>> branch-a are the conflicting +changes trying to be merged. +

+ + + If you have questions, please +<<<<<<< HEAD +open an Issue +======= +ask them in Discussions. +>>>>>>> branch-a + + + A merge conflict + +

+You can then choose which change to retain, deleting all the +extra <<<<<<< HEAD, +=======, and +>>>>>>> branch-a lines. +

+

+However, sometimes the merge conflict is too involved to be +corrected using the web interface. In that situation, you will +need to use a Codespace and follow the instructions at either +Resolving a merge conflict using the command line +or +Using Git source control in VS Code | Merge conflicts.

\ No newline at end of file