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