Merge branch 'master' into master

jramosf · Apr 17, 2019 · 135d86c · 135d86c
2 parents 58dd424 + c45c234
commit 135d86c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -125,5 +125,9 @@ endif
 	@echo "--> Done installing new dependencies"
 	@echo ""
 
+# Execute with make checkout-pr pr=<pr number>
+checkout-pr:
+	git fetch upstream pull/$(pr)/head:pr-$(pr)
+
 
 .PHONY: develop dev-postgres dev-docs setup-git build clean update-submodules test testloop test-cli test-js test-python lint lint-python lint-js coverage publish release