Child pages
  • Deploying from GitHub

Versions Compared


  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Add instructions for deploying with script.


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.

Code Block
titleDeploying 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.

Code Block
titleDeploying 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