diff options
| author | Hugo Herbelin | 2020-10-04 21:51:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-06 21:59:07 +0200 |
| commit | 3b8252d8990e715e5954812dffd0a5986cbb6012 (patch) | |
| tree | 8993a75d8ad87b0bf9cad9de02ddfc5a75f91042 /printing/printer.ml | |
| parent | bd57c1a48cca55be374e597e2d89fe619a39c26e (diff) | |
Documenting option Set Printing Goal Name.
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions