[nongnu] elpa/proof-general e2138d0 3/4: Indentation testing CI ready (hopefully).

[ELPA Syncer]

branch: elpa/proof-general
commit e2138d0b8248ef85d8fb2bc8c89a6c5f33f9f28f
Author: Pierre COURTIEU <pierre.courtieu@cnam.fr>
Commit: Pierre Courtieu <Matafou@users.noreply.github.com>

    Indentation testing CI ready (hopefully).
---
 ci/test-indent/Makefile                            | 22 ++++++++++++++++++++++
 ci/test-indent/coq-test-indent.sh                  | 12 +++++++++---
 .../{indent_equations.v => indent-equations.v}     |  0
 .../{indent_monadic.v => indent-monadic.v}         |  0
 ci/test-indent/tests.sh                            |  1 +
 5 files changed, 32 insertions(+), 3 deletions(-)

diff --git a/ci/test-indent/Makefile b/ci/test-indent/Makefile
new file mode 100644
index 0000000..5aa999a
--- /dev/null
+++ b/ci/test-indent/Makefile
@@ -0,0 +1,22 @@
+# This file is part of Proof General.
+# 
+# © Copyright 2021  Pierre Courtieu
+# 
+# Authors: Pierre Courtieu
+# Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+# 
+# License:     GPL2+ (GNU GENERAL PUBLIC LICENSE)
+
+TESTS:=$(wildcard indent-*.v)
+INDENTED:=$(subst indent-,indented_indent-, $(TESTS))
+
+all: $(INDENTED)
+
+indented_%.v: %.v
+       @echo "### testing indentation of $<..."
+       @./coq-test-indent.sh $<
+
+.PHONY: clean
+
+clean:
+       rm -f indented_indent*
diff --git a/ci/test-indent/coq-test-indent.sh 
b/ci/test-indent/coq-test-indent.sh
index 7204d00..2f35397 100755
--- a/ci/test-indent/coq-test-indent.sh
+++ b/ci/test-indent/coq-test-indent.sh
@@ -1,3 +1,4 @@
+#!/bin/bash
 
 # This script should be launched from its own directory, so that file
 # coq-test-indent.el is accessible.
@@ -24,14 +25,19 @@ emacs -q -batch --eval "(progn (load-file 
\"coq-test-indent.el\") (launch-test \
 # echo "grep \"INDENT CHANGED\" $INDENTEDTESTFILE"
 # grep "INDENT CHANGED" $INDENTEDTESTFILE
 echo -n " diff -q $TESTFILE $INDENTEDTESTFILE..."
-diff -q $TESTFILE $INDENTEDTESTFILE > /dev/null
-if [[ $? == 1 ]] ;
+diff -q $TESTFILE $INDENTEDTESTFILE
+if [[ "$?" == 1 ]] ;
 then echo " DIFFERENCES FOUND" 
+     diff -u $TESTFILE $INDENTEDTESTFILE
      printf "${RED} TEST FAILURE ***${NC}\n"
-     echo "  *** details can be seen with:"
+     echo "  *** details can be seen by reproducing the tests:"
+     echo "  *** cd ci/test-indent"
+     echo "  *** make"
      echo "  ***  diff --side-by-side --suppress-common-lines $TESTFILE 
$INDENTEDTESTFILE"
      echo "  *** or graphically: "
      echo "  ***  meld $TESTFILE $INDENTEDTESTFILE"
+     exit 1 # Make the test program fail, so that CI knows.
 else echo "NO DIFFERENCE"
      printf "${GREEN} TEST SUCCESS *** ${NC}\n"
+     exit 0
 fi
diff --git a/ci/test-indent/indent_equations.v 
b/ci/test-indent/indent-equations.v
similarity index 100%
rename from ci/test-indent/indent_equations.v
rename to ci/test-indent/indent-equations.v
diff --git a/ci/test-indent/indent_monadic.v b/ci/test-indent/indent-monadic.v
similarity index 100%
rename from ci/test-indent/indent_monadic.v
rename to ci/test-indent/indent-monadic.v
diff --git a/ci/test-indent/tests.sh b/ci/test-indent/tests.sh
index 9dcd5c0..ef2c23e 100755
--- a/ci/test-indent/tests.sh
+++ b/ci/test-indent/tests.sh
@@ -1,3 +1,4 @@
+#!/bin/bash