1.2 KiB
						
					
					
				
			
		
		
		
			
			
			
				
					
				
				
					
				
			
		
		
	
	The following steps should be performed to integrate pull requests from Github.
- 
After a pull request is opened, some automatic build checks should be performed by Github Actions. Failures of these checks should be fixed. 
- 
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.)
- ...
 
- 
Integrate the pull request via Github, preferably by rebase and merge. 
- 
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
- 
Fetch the current Github master: git fetch github
- 
Make sure to be on the (internal) master: git checkout master
- 
Rebase the changes of Github onto the (internal) master: git rebase github/master
- 
Check that Storm builds successfully and everything works as expected. 
- 
Push the changes into the internal repository: git push origin