diff options
author | Neels Hofmeyr <nhofmeyr@sysmocom.de> | 2016-10-01 01:47:16 +0200 |
---|---|---|
committer | Neels Hofmeyr <nhofmeyr@sysmocom.de> | 2016-10-01 01:58:47 +0200 |
commit | b497b36543d2ed0fd0266cf42f8e4a908ee3ed10 (patch) | |
tree | 82a9f81d50f17dbc9cb6e5940c327db24f581487 /coverity | |
parent | 9c5feb21c48e78ea029da40d697df86e1d8eaf1c (diff) |
coverity: add jenkins.sh as explicit build server entry point
During the recent refactorings, I need to edit the jenkins build config at the
right time to apply renames. To make this easier in the future, add an explicit
(so far trivial) entry point for jenkins that can just be updated from git.
Change-Id: I8de9444df513b3aaaddb07b383e458186237dfab
Diffstat (limited to 'coverity')
-rwxr-xr-x | coverity/jenkins.sh | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/coverity/jenkins.sh b/coverity/jenkins.sh new file mode 100755 index 0000000..9adfe99 --- /dev/null +++ b/coverity/jenkins.sh @@ -0,0 +1,2 @@ +#!/bin/sh +./coverity_Osmocom.sh |