diff options
Diffstat (limited to 'academic/octave/patches/compressed-info.diff')
| -rw-r--r-- | academic/octave/patches/compressed-info.diff | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/academic/octave/patches/compressed-info.diff b/academic/octave/patches/compressed-info.diff new file mode 100644 index 0000000000..48178d773f --- /dev/null +++ b/academic/octave/patches/compressed-info.diff @@ -0,0 +1,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 |