diff options
Diffstat (limited to 'src/make.configuration.deps')
| -rw-r--r-- | src/make.configuration.deps | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/make.configuration.deps b/src/make.configuration.deps index ba81ac3..4ccfd1f 100644 --- a/src/make.configuration.deps +++ b/src/make.configuration.deps @@ -318,10 +318,11 @@ CONFIG-ID-FILE = $(TOP)/CONFIG-ID git-push-everything: git-commit-everything $(BUILD-ID-FILE) { \ '$(GIT-BIN)/git-init-master-repo.pl' '$(GIT)' '$(GIT-MASTER-REPO)' && \ + eval "$$('$(GIT-BIN)/git-get-localdir.pl' '$(GIT)')" && \ if [ -e "$(CCTK_HOME)/cactus.config" ]; then \ - . "$(CCTK_HOME)/cactus.config"; \ + source "$(CCTK_HOME)/cactus.config"; \ fi && \ - export CACTUS_CENTRAL_GIT_REPO && \ + export CACTUS_LOCAL_GIT_REPO CACTUS_CENTRAL_GIT_REPO && \ '$(GIT-BIN)/git-push-everything.pl' '$(GIT)' '$(GIT-REPO)' '$(GIT-MASTER-REPO)'; \ } || echo "Formaline: WARNING: Error while pushing to master repository" |