Merge remote-tracking branch 'origin/devel' into devel

frankmayer · frankmayer · commit 43b15fca1cab · 2017-02-10T14:48:06.000+02:00
diff --git a/.travis.yml b/.travis.yml
@@ -14,3 +14,6 @@ before_script:
 
 script: 
   - phpunit --configuration ./tests/phpunit.xml
+
+after_script:
+  - ./tests/travis/teardown_arangodb.sh
diff --git a/tests/travis/teardown_arangodb.sh b/tests/travis/teardown_arangodb.sh
@@ -0,0 +1,9 @@
+
+ARCH=$(arch)
+if [ "$ARCH" == "x86_64" ]; then
+  ARANGOD="arangod_x86_64"
+else
+  ARANGOD="arangod"
+fi
+echo "killing arangod binary ${ARANGOD}"
+killall -9 "${ARANGOD}" || true
