allow ill-formed documentation strings

General Forms:
(set-ignore-doc-string-error nil)   ; :doc strings must be well-formed
(set-ignore-doc-string-error t)     ; ill-formed :doc strings are ignored
(set-ignore-doc-string-error :warn) ; ill-formed :doc strings are ignored
                                    ;   except for causing a warning
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.

General Form:
(set-ignore-doc-string-error flag)
where flag is nil, t, or :warn, as indicated above. This macro is essentially equivalent to
(table acl2-defaults-table :ignore-doc-string-error flag)
and hence is local to any books and encapsulate events in which it occurs; see acl2-defaults-table. However, unlike the above simple call of the table event function (see table), no output results from a set-ignore-doc-string-error event.

Note that since defdoc events have the sole purpose of installing documentation strings, these require well-formed documentation strings even after executing a call of ignore-doc-string-error.

The default behavior of the system is as though the :ignore-doc-string-error value is nil. The current behavior can be ascertained by evaluating the following form.

(ignore-doc-string-error (w state))