Deploying from GitHub

Usually when deploying from GitHub, you can just run the script stardeploy.sh from https://svn.divms.uiowa.edu/repos/clc/projects/starexec/util. In this case, to deploy a particular tag, the tag name is passed as an argument to the script.

./stardeploy.sh $TAG_NAME

Deploying Manually

In cases where stardeploy.sh 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.

# This first step can be skipped if an existing clone exists on disk (from a previous deploy)
git clone -- https://github.com/StarExec/StarExec.git 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

script/soft-deploy.sh

Related articles

• Page:
  Deploying from GitHub
• Page:
  Tagging for deploy
• Page:
  Deployment