Major Section: OTHER
Examples: ACL2 !>(good-bye) ; [ACL2 is exited] ACL2 !>(good-bye 3) ; [ACL2 is exited with Unix exit status 3]Note: Your entire session will disappear forever when you evaluate
(good-bye).
The command (good-bye) quits not only out of the ACL2 command loop,
but in fact quits entirely out of the underlying Lisp. Thus, there
is no going back! You will not be able to re-enter the command loop
after typing (good-bye)! All your work will be lost!!!
This command may not work in some underlying Common Lisp implementations. In such cases, there is no harm in trying; ACL2 will let you know how to proceed if it cannot exit.
In some systems, typing control-d at the top-level ACL2 prompt
(control-c control-d if inside emacs) will call this function.
If you give good-bye an argument, it should be a natural number, and it
indicates the Unix (Linux) exit status.
If you merely want to exit the ACL2 command loop, use :q instead
(see q).
