diff --git a/Makefile b/Makefile index 34bf1cb43..89cda4a4e 100644 --- a/Makefile +++ b/Makefile @@ -404,6 +404,14 @@ new-develop: $(NEW_DEVELOP) mkdir -p $(DEVELOP) $(MAKE) develop/.current +.PHONY: switch-develop +# HELP: switch current develop instance to DEVELOP=... +switch-develop: + if ! [ -e develop/$(DEVELOP) ]; then \ + echo "Specified develop $(DEVELOP) does not exist! Not switching." ; \ + exit 1 ; \ + fi ; \ + echo "$(DEVELOP)" > develop/.current .PHONY: --develop --develop: if ! [[ -e develop ]]; then \