1
0
mirror of https://github.com/gsi-upm/senpy synced 2025-09-18 04:22:21 +00:00

Compare commits

...

2 Commits

Author SHA1 Message Date
J. Fernando Sánchez
f6bf7459a8 Added push to github in fix-makefiles 2017-10-03 16:41:04 +02:00
J. Fernando Sánchez
300f4c374a Trying to fix push to github 2017-10-03 16:39:09 +02:00
2 changed files with 4 additions and 3 deletions

View File

@@ -63,6 +63,7 @@ push-github:
only: only:
- master - master
- triggers - triggers
- fix-makefiles
deploy_pypi: deploy_pypi:
stage: deploy stage: deploy

View File

@@ -13,12 +13,12 @@ git-pull:
push-github: ## Push the code to github. You need to set up GITHUB_DEPLOY_KEY push-github: ## Push the code to github. You need to set up GITHUB_DEPLOY_KEY
ifeq ($(GITHUB_DEPLOY_KEY),) ifeq ($(GITHUB_DEPLOY_KEY),)
else else
$(eval KEY_FILE := $(shell mktemp)) $(eval KEY_FILE := "$(shell mktemp)")
@echo "$(GITHUB_DEPLOY_KEY)" > $(KEY_FILE) @echo "$(GITHUB_DEPLOY_KEY)" > $(KEY_FILE)
@git remote rm github-deploy || true @git remote rm github-deploy || true
git remote add github-deploy $(GITHUB_REPO) git remote add github-deploy $(GITHUB_REPO)
@GIT_SSH_COMMAND="ssh -i $(KEY_FILE)" git fetch github-deploy $(CI_COMMIT_REF_NAME) || true -@GIT_SSH_COMMAND="ssh -i $(KEY_FILE)" git fetch github-deploy $(CI_COMMIT_REF_NAME)
@GIT_SSH_COMMAND="ssh -i $(KEY_FILE)" git push github-deploy $(CI_COMMIT_REF_NAME) @GIT_SSH_COMMAND="ssh -i $(KEY_FILE)" git push github-deploy HEAD:$(CI_COMMIT_REF_NAME)
rm $(KEY_FILE) rm $(KEY_FILE)
endif endif