Double escape.

dealii · Mar 8, 2023 · 254b976 · 254b976
1 parent 8047da9
commit 254b976
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Jenkinsfile b/Jenkinsfile
@@ -69,8 +69,8 @@ pipeline
               for f in publications-*.bib ; do \
                 bibtool -q -r bibtool.rsc -i ./$f -o ./$f || exit 1 ; \
               done
-              git diff --ignore-blank-lines -I\"% Encoding: US-ASCII\" -I\"@Comment{jabref-meta: databaseType:bibtex;}\"
-              git diff-files --ignore-blank-lines -I\"% Encoding: US-ASCII\" -I\"@Comment{jabref-meta: databaseType:bibtex;}\" --quiet || exit $?
+              git diff --ignore-blank-lines -I\\"% Encoding: US-ASCII\" -I\\"@Comment{jabref-meta: databaseType:bibtex;}\\"
+              git diff-files --ignore-blank-lines -I\\"% Encoding: US-ASCII\\" -I\\"@Comment{jabref-meta: databaseType:bibtex;}\\" --quiet || exit $?
               git reset --hard
             '''
           }