diff --git a/marketplace/scribblings/Makefile b/marketplace/scribblings/Makefile index ba1a57a..e95a9b8 100644 --- a/marketplace/scribblings/Makefile +++ b/marketplace/scribblings/Makefile @@ -1,6 +1,11 @@ all: out pages: + @(git branch -v | grep -q gh-pages || (echo local gh-pages branch missing; false)) + @echo + @git branch -av | grep gh-pages + @echo + @(echo 'Is the branch up to date? Press enter to continue.'; read dummy) git clone -b gh-pages ../.. pages publish: out pages