ACL2-PC::EX

(macro) exit after possibly saving the state
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
ex

Same as exit, except that first the instruction save is executed.

If save queries the user and is answered negatively, then the exit is aborted.