From 3f9616d3e069778a84c5badb636ae8d6b4e94084 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 1 Mar 2021 18:10:26 +0100
Subject: [PATCH] Added documentation about integrating Github pull requests

---
 doc/merge_pull_requests.md | 39 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 doc/merge_pull_requests.md

diff --git a/doc/merge_pull_requests.md b/doc/merge_pull_requests.md
new file mode 100644
index 000000000..77fed308a
--- /dev/null
+++ b/doc/merge_pull_requests.md
@@ -0,0 +1,39 @@
+The following steps should be performed to integrate pull requests from Github.
+
+0. After a pull request is opened, some automatic build checks should be performed by Github Actions.
+   Failures of these checks should be fixed.
+
+1. 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.)
+   * ...
+
+2. Integrate the pull request via Github, preferably by *rebase and merge*.
+
+3. Optional (if not done already): add the Github repository as another remote for your local copy of the internal repository:
+   ```console
+   git remote add github https://github.com/moves-rwth/storm.git
+   ```
+   
+4. Fetch the current Github master:
+   ```console
+   git fetch github
+   ```
+
+5. Make sure to be on the (internal) master:
+   ```console
+   git checkout master
+   ```
+
+6. Rebase the changes of Github onto the (internal) master:
+   ```console
+   git rebase github/master
+   ```
+
+7. Check that Storm builds successfully and everything works as expected.
+
+8. Push the changes into the internal repository:
+   ```console
+   git push origin
+   ```