Child pages
  • Deploying from GitHub

Usually when deploying from GitHub, you can just run the script from In this case, to deploy a particular tag, the tag name is passed as an argument to the script.

Deploying with

Deploying Manually

In cases where is not used, it is possible to deploy manually by following these steps.

Make sure that $STAREXEC_CONFIG refers to a properties file with your specific deploy configuration.

Deploying Manually
# This first step can be skipped if an existing clone exists on disk (from a previous deploy)
git clone -- StarExec-deploy # Clone the GitHub repository if no existing clone exists

cd StarExec-deploy
git fetch origin $TAG_NAME
git checkout $TAG_NAME -B deploy

ant -propertyfile "$STAREXEC_CONFIG" build
ant reload-sql update-sql