commit 29db0fd994138d31b17e7a01faef3bfbdbd43538
author Davide Pesavento <davide.pesavento@lip6.fr> Tue Aug 29 13:32:00 2017 -0400
committer Davide Pesavento <davide.pesavento@lip6.fr> Sat Sep 02 22:31:55 2017 -0400
tree 82c5606c8f9233e3b7838d9c5305a07c76b5edb7
parent 9a47123529eedea2e51f0cf72160ae419ad8e582

Sync build system and CI scripts with ndn-tools

Change-Id: I21dc5349f3f3c819bf8590fe709157ce0bc26b44

.jenkins

diff --git a/.jenkins b/.jenkins
index 4daa40f..674d751 100755
--- a/.jenkins
+++ b/.jenkins
@@ -1,9 +1,10 @@
 #!/usr/bin/env bash
 set -e
 
-DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
 
-for i in `find "$DIR/.jenkins.d" -type f -perm +111 | sort`; do
-    echo "Run: $i"
-    $i
+for file in "$DIR"/.jenkins.d/*; do
+    [[ -f $file && -x $file ]] || continue
+    echo "Run: $file"
+    "$file"
 done