16 lines
		
	
	
	
		
			320 B
		
	
	
	
		
			Text
		
	
	
	
	
	
		
		
			
		
	
	
			16 lines
		
	
	
	
		
			320 B
		
	
	
	
		
			Text
		
	
	
	
	
	
| 
								 | 
							
								#!/bin/bash
							 | 
						||
| 
								 | 
							
								set -e
							 | 
						||
| 
								 | 
							
								set -x
							 | 
						||
| 
								 | 
							
								
							 | 
						||
| 
								 | 
							
								if ! git diff-index --quiet HEAD; then
							 | 
						||
| 
								 | 
							
								    set +x
							 | 
						||
| 
								 | 
							
								    echo "There are uncommitted changes:"
							 | 
						||
| 
								 | 
							
								    git status --short
							 | 
						||
| 
								 | 
							
								    echo "Doing nothing to avoid losing your work."
							 | 
						||
| 
								 | 
							
								    exit 1
							 | 
						||
| 
								 | 
							
								fi
							 | 
						||
| 
								 | 
							
								request_id="$1"
							 | 
						||
| 
								 | 
							
								remote=${2:-"upstream"}
							 | 
						||
| 
								 | 
							
								git fetch "$remote" "pull/$request_id/head"
							 | 
						||
| 
								 | 
							
								git reset --hard FETCH_HEAD
							 |