Write strings to a file when not allowed without a trust tag.
;; Writes the STRINGS to file FILENAME, overwriting its previous contents. ;; Effectively, all the STRINGS get concatenated and the result becomes the new ;; contents of the file. Returns (mv erp state). CTX is a context for error ;; printing. The ttag is needed because this calls open-output-channel!, but ;; that makes this version usable during make-event expansion, ;; clause-processors, etc. (defund write-strings-to-file! (strings filename ctx state) (declare (xargs :stobjs state :guard (and (string-listp strings) (stringp filename)))) (mv-let (channel state) (open-output-channel! filename :character state) (if (not channel) (prog2$ (er hard? ctx "Unable to open file ~s0 for :character output." filename) (mv t state)) (pprogn (write-strings-to-channel strings channel state) (close-output-channel channel state) (mv nil state)))))