You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 

1.2 KiB

The following steps should be performed to integrate pull requests from Github.

  1. After a pull request is opened, some automatic build checks should be performed by Github Actions. Failures of these checks should be fixed.

  2. Manually review the pull request on Github and suggest improvements if necessary. In particular make sure:

    • No unnecessary files were committed (for example build artefacts, etc.)
    • No remains from the development are present (for example debug output, hackish workarounds, etc.)
    • ...
  3. Integrate the pull request via Github, preferably by rebase and merge.

  4. Optional (if not done already): add the Github repository as another remote for your local copy of the internal repository:

    git remote add github https://github.com/moves-rwth/storm.git
    
  5. Fetch the current Github master:

    git fetch github
    
  6. Make sure to be on the (internal) master:

    git checkout master
    
  7. Rebase the changes of Github onto the (internal) master:

    git rebase github/master
    
  8. Check that Storm builds successfully and everything works as expected.

  9. Push the changes into the internal repository:

    git push origin