Choose the Polyspace Metrics server to be used in this project, as defined on the Configure System page.
You can then use these variables in scripts in the Build section of this project. For instance, in a Shell script, use these variables with the syntax $VAR
. In a Windows batch file, use the syntax %VAR%
.
POLYSPACE_METRICS_HOST
is the hostname of the Polyspace Metrics server.POLYSPACE_METRICS_PORT
is the port number of the Polyspace Metrics server.POLYSPACE_METRICS_URL
is the URL of the Polyspace Metrics server.ps_helper_metrics_upload
is a helper utlity to upload Polyspace results to the specified server.
Syntax (shell scripts):
$ps_helper_metrics_upload ResultsDirwhere
ResultsDir
is a folder containing Polyspace results.