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