summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorvlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4>2015-07-02 00:17:00 +0000
committervlefevre <vlefevre@280ebfd0-de03-0410-8827-d642c229c3f4>2015-07-02 00:17:00 +0000
commit7833a4964a7e0b4fb4d299ce350b082c181793f5 (patch)
tree684a663f90718d5246a96436b23302299f026a48
parent9c8743683afc599b185f3a26ef127ca5fc2ad971 (diff)
downloadmpfr-7833a4964a7e0b4fb4d299ce350b082c181793f5.tar.gz
[tools/mpfrlint] Check a Texinfo rule (Section "Ending a Sentence")
with common words that end with a capital letter. (merged changeset r9603 from the 3.1 branch) git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@9604 280ebfd0-de03-0410-8827-d642c229c3f4
-rwxr-xr-xtools/mpfrlint7
1 files changed, 7 insertions, 0 deletions
diff --git a/tools/mpfrlint b/tools/mpfrlint
index 51e1c1c61..dc5e6d75d 100755
--- a/tools/mpfrlint
+++ b/tools/mpfrlint
@@ -134,6 +134,13 @@ do
echo "$file contains unprotected mpfr_printf-like function calls"
done
+# Check a Texinfo rule (Section "Ending a Sentence") with common words
+# that end with a capital letter:
+# Use '@.' instead of a period, '@!' instead of an exclamation point,
+# and '@?' instead of a question mark at the end of a sentence that
+# does end with a capital letter.
+grep -E '(LIP|MPFR?|NaN)\)?[.!?]' doc/mpfr.texi | grep -v '^\* .*::'
+
fdlv1="`sed -n '/Version / {
s/.*Version //
s/,.*//