| Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
anyway wrong technique). Instead use inhibit-read-only to allow write
in possibly read-only area.
|
|
span-write-warning: don't call FUN if inhibit-read-only.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
improvements
|
|
proof-script
|
|
|
|
|
|
|
|
under fontconfig (i.e. existence of smoothly rendering free fonts with
same metrics)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
commands (certainly when the value is persisted).
|
|
|
|
|
|
pre-processing of commands when they're queued from script
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(mask current bug in Coq code)
|
|
Don't turn on holes in shell
|
|
|
|
|
|
|
|
|
|
|
|
|