Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <01847-0@swan.cl.cam.ac.uk>; Thu, 17 Oct 1991 13:24:05 +0100
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA15154;
          Thu, 17 Oct 91 05:17:24 pdt
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from [128.232.0.56] by ted.cs.uidaho.edu (15.11/1.34) id AA15150;
          Thu, 17 Oct 91 05:17:17 pdt
Received: from coot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <01632-0@swan.cl.cam.ac.uk>; Thu, 17 Oct 1991 13:14:12 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: bug in HOL version 2.
Date: Thu, 17 Oct 91 13:14:04 +0100
From: Paul.Curzon@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.654:17.09.91.12.15.33"@cl.cam.ac.uk>


-----------------------------------------------------
BUG REPORT: the more_arithmetic and more_list library
            Makefiles in version 2.0
-----------------------------------------------------

There is, unfortunately, a bug in the Makefile of the
more_arithmetic library in the newly released HOL version 2. Some of
the entries contain `quit()` instead of `quit();;`. There is also a
mistake in the more_lists library Makefile where `quit();;;;` has
been used instead of `quit();;`  This has been repaired for version
2.01. To fix the bugs in version 2, change the lines:

             'quit()' | ${Hol}

in the file hol/Library/more_arithmetic/Makefile to

             'quit();;' | ${Hol}

and the line

             'quit();;;;' | ${Hol}

in the file hol/Library/more_lists/Makefile to

             'quit();;' | ${Hol}

You should then be able to build the libraries.

Paul.