Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 15 Mar 1994 13:13:37 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03774; Tue, 15 Mar 1994 05:53:57 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA03770; Tue, 15 Mar 1994 05:53:42 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 15 Mar 1994 12:53:29 +0000 To: info-hol@leopard.cs.byu.edu Subject: Gzip for compression Date: Tue, 15 Mar 94 12:53:23 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:060470:940315125351"@cl.cam.ac.uk> The HOL distribution areas contain quite a lot of compressed files, and I'd like to move to using "gzip" instead of "compress". It usually results in a much better compression ratio -- for example a gzip of the current HOL system is about 60% of the size of a compressed version. I am only hesitating because I'm wondering how widespread gzip is. Certainly it's not as "standard" as compress, though one of our systems people tells me that this situation is likely to be reversed in the future, since compress uses a patented algorithm. So, does anyone object to my making this change? John.