PROMPT

the prompt printed by ld
Major Section:  MISCELLANEOUS

The prompt printed by ACL2 conveys information about various ``modes.'' See default-print-prompt and see ld-prompt for details.