# HG changeset patch
# User Mike Miller <mtmiller@ieee.org>
# Date 1388583823 18000
# Node ID ab775508dff9d54266e5cb8f965201298a11d66f
# Parent  d638db6d045cef65a529ce1a232da22443806805
doc.m: Check for existence of compressed info file (bug #41054)

* doc.m: Check for existence of compressed info file, since info files
are commonly gzip-compressed in binary distributions.

diff -r d638db6d045c -r ab775508dff9 scripts/help/doc.m
--- a/scripts/help/doc.m	Wed Jan 01 18:24:55 2014 -0800
+++ b/scripts/help/doc.m	Wed Jan 01 08:43:43 2014 -0500
@@ -80,7 +80,8 @@
       if (err < 0)
         info_file_name = info_file ();
 
-        if (! exist (info_file_name, "file"))
+        if (! exist (info_file_name, "file")
+            && ! exist ([info_file_name ".gz"], "file"))
           __gripe_missing_component__ ("doc", "info-file");
         endif
       endif