RE: [Gcl-devel] 2.6.2.....

[Mike Thomas]

Hi Matt.

| Just a comment you and Camm can use or ignore as you choose....
|
| We maintain ACL2 in a manner such that the workshop books are all
| expected to
| certify.  When I'm testing a local ACL2 build, I typically run the full
| regression suite (including the workshop books) and I expect 100% to pass.

I would rather fullfil your expectations vis-a-vis pass/fail and from the
little I know of him I expect Camm would also take this view.

This means that we should extend the Linux testing to cover those workshop
books too if someone hasn't already done so.  I can't follow up in detail on
this failure at present.

| Perhaps the failure was just some weird Windows glitch, which
| would go away in
| a re-run?

I doubt it (Windows isn't that unpredictable you know!!), but I'm doing a
check rerun and will report later.

Cheers

Mike Thomas.