diff options
| author | Pierre Courtieu | 2017-04-26 11:57:58 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2017-05-04 11:13:49 +0200 |
| commit | 1fe73e6af81759fa8b78c8660745492ed886d477 (patch) | |
| tree | 4847f56a199aa1f2cd433b3f0c1d791563634fbe /dev/include | |
| parent | 773d95f915996b581b7ea82d9193197649c951a0 (diff) | |
Adding an option "Printing Unfocused".
Off by default.
+ small refactoring of emacs hacks in printer.ml.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions