From 82ee6b5012745fe3375891029d81a20e5fe240db Mon Sep 17 00:00:00 2001
From: Rolf Bjarne Kvinge <rolf@xamarin.com>
Date: Wed, 18 May 2016 18:41:07 +0200
Subject: [PATCH] [jenkins] Add initial script to execute on jenkins.

---
 jenkins.sh | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100755 jenkins.sh

diff --git a/jenkins.sh b/jenkins.sh
new file mode 100755
index 000000000000..78c1444dbf84
--- /dev/null
+++ b/jenkins.sh
@@ -0,0 +1,4 @@
+#!/bin/bash -e
+
+./configure
+time make world