Has the command line info utility used to read info files from the command line been depricated and removed from debian? --