commit | b497b36543d2ed0fd0266cf42f8e4a908ee3ed10 | [log] [tgz] |
---|---|---|
author | Neels Hofmeyr <nhofmeyr@sysmocom.de> | Sat Oct 01 01:47:16 2016 +0200 |
committer | Neels Hofmeyr <nhofmeyr@sysmocom.de> | Sat Oct 01 01:58:47 2016 +0200 |
tree | 82a9f81d50f17dbc9cb6e5940c327db24f581487 | |
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