blob: 48178d773f1e9f21b1e36203b90b144ec3baa9e1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
diff --git a/scripts/help/doc.m b/scripts/help/doc.m
--- a/scripts/help/doc.m
+++ b/scripts/help/doc.m
@@ -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
|
