[acl2/acl2] 14d07a: Change two backquotes to ordinary quotes, to work ...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 14d07aa39cbefe5055dd20a2cb9cc1d3681ccb89
https://github.com/acl2/acl2/commit/14d07aa39cbefe5055dd20a2cb9cc1d3681ccb89
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2017-08-16 (Wed, 16 Aug 2017)

Changed paths:
M books/projects/x86isa/machine/x86.lisp

Log Message:
-----------
Change two backquotes to ordinary quotes, to work around apparent SBCL bug.

The bug was on linux, and was causing regressions to fail when books
attempted to include books/projects/x86isa/machine/x86.lisp. It
didn't seem to happen with SBCL 1.3.11 but it did with SBCL 1.3.19 and
1.3.20. I plan to send a bug report on Friday (as after considerable
effort, I've distilled the problem down so that ACL2 isn't necessary),
but this change suffices as a workaround.

[GitHub]

Branch: refs/heads/testing