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 <02098-0@swan.cl.cam.ac.uk>; Tue, 15 Oct 1991 16:56:14 +0100
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (15.11/1.34) id AA28099;
          Tue, 15 Oct 91 08:41:36 pdt
Received: from cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <01622-0@swan.cl.cam.ac.uk>; Tue, 15 Oct 1991 16:41:46 +0100
To: info-hol@edu.uidaho.cs.ted
Subject: bug in HOL version 2.
Date: Tue, 15 Oct 91 16:41:42 +0100
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.624:15.09.91.15.41.48"@cl.cam.ac.uk>

-------------------------------------------------
BUG REPORT: the "install" function in version 2.0
-------------------------------------------------

There is, unfortunately, a bug in the install function in the
newly released HOL version 2.  The function incorrectly sets the
help search path.  This has now been repaired for version 2.01,
but users of version 2 may wish to incorporate the following patch
into their system.  To fix the bug, change the line:

       let helps = [`/ENTRIES/`] in

in the definition of install in the file hol/ml/gen.ml to:

       let helps = [`/help/ENTRIES/`] in

and then rebuild your system.

In the absence of this patch, the system can also be installed correctly
by using set_help_search_path after using install.

Tom