From 586f0cce7b362380dfbe1753ab9480e435529b06 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 22 Apr 2017 14:19:59 +0200
Subject: [PATCH] sanity: ensure all binaries are documented

* tests/sanity/bin.test: New file.
* tests/Makefile.am: Run it.
---
 tests/Makefile.am     |  1 +
 tests/sanity/bin.test | 77 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 78 insertions(+)
 create mode 100644 tests/sanity/bin.test

diff --git a/tests/Makefile.am b/tests/Makefile.am
index 3f43232e5..dac18ae83 100644
--- a/tests/Makefile.am
+++ b/tests/Makefile.am
@@ -409,6 +409,7 @@ endif
 
 TESTS_sanity = \
   sanity/80columns.test \
+  sanity/bin.test \
   sanity/includes.test \
   sanity/ipynb.pl \
   sanity/private.test \
diff --git a/tests/sanity/bin.test b/tests/sanity/bin.test
new file mode 100644
index 000000000..2572d9e06
--- /dev/null
+++ b/tests/sanity/bin.test
@@ -0,0 +1,77 @@
+#! /bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2017 Laboratoire de Recherche et Développement de
+# l'Epita (LRDE).
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+set +x
+
+exit_status=0
+
+for binary in "$top_builddir"/bin/*
+do
+    test -f "$binary" || continue
+    test -x "$binary" || continue
+    case $binary in
+        *.py) continue
+    esac
+    binary=${binary##*/}
+
+    # All binaries should have a man page
+    manpage=
+    # Man pages are built in builddir, but as we distribute
+    # them they may also be in srcdir.
+    for man in "$top_srcdir"/bin/man/$binary.* \
+               "$top_builddir"/bin/man/$binary.*; do
+        case $man in
+            *.[0-9]) manpage=${man##*/};;
+        esac
+    done
+    if test -z $manpage; then
+        echo "bin/$binary has no man page"
+        exit_status=2
+    else
+        if ! grep -q "man/${manpage}.html" $top_srcdir/doc/org/tools.org; then
+            echo "bin/man/$manpage is not listed in doc/org/tools.org"
+            exit_status=2
+        fi
+        if ! grep -q "$manpage" $top_srcdir/bin/man/Makefile.am; then
+            echo "bin/man/$manpage is not listed in man/Makefile.am"
+            exit_status=2
+        fi
+    fi
+
+    # All man pages
+    case $manpage in
+        *.1)
+            if ! test -f $top_srcdir/doc/org/$binary.org; then
+                echo "bin/$binary has no doc/org/$binary.org page"
+                exit_status=2
+            else
+                if ! grep -q "${binary}.org" $top_srcdir/doc/org/tools.org; then
+                    echo "${binary}.org is not listed in doc/org/tools.org page"
+                    exit_status=2
+                fi
+                if ! grep -q "${binary}.org" $top_srcdir/doc/Makefile.am; then
+                    echo "${binary}.org does not occur in doc/Makefile.am"
+                    exit_status=2
+                fi
+            fi
+    esac
+done
+
+exit $exit_status