Skip to end of metadata
Go to start of metadata

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 9 Next »

Overview

Instructions for implementing a feature (e.g. new functionality, bug fix, documentation).

Setup

Configure Git with your name and email: https://linuxize.com/post/how-to-configure-git-username-and-email/

  • --global if you want to use it as the default, otherwise it will just be for the current repository

  • You can use your anonymous GitHub no-reply email

Ensure core.autocrlf is set to true or input . Line endings on GitHub are LF only, not CRLF!

Instructions

Make sure anything on the current branch has been saved, either through commit or stash.

Create a new branch from main:

git status  # Working tree should be clean, otherwise save or discard the modified file(s)
git checkout main
git pull
git checkout -b new-branch-name

Commits

Commits are small changes you make so that you can track your progress and experiment without fear of losing previous work. It is better to commit early and often!

git status
git add [file name]  # To stage for commit, repeat as necessary, period to add all files
git commit -m "[description of change]"
git push

Pull Request

A pull request is a request to merge the changes on the current branch into the main branch.

Requirements:

  • Test cases (including unit tests) have been written

  • Documentation and comments have been written

  • No new TODOs. If there are, a written comment with a clear explanation of why it cannot be resolved

  • Formatting follows the style guide and generally passes linting

  • Functionality works for all use cases

    • Your code should work to the best of your ability; no one wants to deal with fixing code that’s “good enough” or “works most of the time” when they’re trying to focus on their own code

Get the latest changes from main branch and either merge or rebase so your branch is up to date:

git fetch main
# Pick one of the following:
git merge main  # Easier but destroys your history
git rebase main  # More annoying (especially if you have a lot of commits) but keeps clear history

On the repository GitHub, create a pull request (using your branch name) with a descriptive title and body outlining the changes. Don’t forget to click the create button!

Copy the new pull request link, which is numbered.

On the Discord server, ping an Autonomy lead with your pull request link asking for review.

The reviewer leaves comments which you need to address (e.g. by making additional commits fixing the issue, leaving another comment explanation, meeting, etc.). Repeat.

Once the reviewer is satisfied, your pull request is approved.

Make sure to squash and merge your changes.

Delete your branch.

In Git, checkout and pull main branch:

git checkout main
git pull

Your changes are now merged!

  • No labels