Updates for new CI

2025-11-19 11:15:49 +00:00 · 2017-11-13 15:53:27 -08:00
parent 764236dd9f
commit 874b871422
5 changed files with 62 additions and 11 deletions
--- a/tool/jenkins.sh
+++ b/tool/jenkins.sh
@@ -0,0 +1,8 @@
+#!/bin/bash
+
+# meant to be run from the root directory of the repo
+
+set -e
+
+tool/conflictmarkers.sh
+tool/all-target-link-checker.sh