changeset 18190:ab775508dff9 stable

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.
author Mike Miller <mtmiller@ieee.org>
date Wed, 01 Jan 2014 08:43:43 -0500
parents d638db6d045c
children f80d258a2c7d
files scripts/help/doc.m
diffstat 1 files changed, 2 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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