# It seems that recent versions of yelp, upon which the gui relies to display the reference
# manual, are broken. It only works on compressed info files. So we must compress them.
# It seems that recent versions of yelp, upon which the gui relies to display the reference
# manual, are broken. It only works on compressed info files. So we must compress them.