From 04940f9bb6778b0cb671356b63bb695f1511bbe2 Mon Sep 17 00:00:00 2001
From: Lars Bilke <lars.bilke@ufz.de>
Date: Fri, 7 Jun 2019 15:16:25 +0200
Subject: [PATCH] [Jenkins] Don't git check .dat files.
---
Jenkinsfile | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/Jenkinsfile b/Jenkinsfile
index 62b7581438b..bdf48fa2a7e 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -28,7 +28,7 @@ pipeline {
agent { label "master"}
steps {
sh "git config core.whitespace -blank-at-eof"
- sh "git diff --check `git merge-base origin/master HEAD` HEAD -- . ':!*.md' ':!*.pandoc' ':!*.asc'"
+ sh "git diff --check `git merge-base origin/master HEAD` HEAD -- . ':!*.md' ':!*.pandoc' ':!*.asc' ':!*.dat'"
dir('scripts/jenkins') { stash(name: 'known_hosts', includes: 'known_hosts') }
ciSkip action: 'check' // Check for [ci skip] or [web] commit message.
--
GitLab