diff options
| author | Arnaud Spiwack | 2015-03-19 13:38:58 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-03-31 11:28:18 +0200 |
| commit | 82abccdc576e3eff3adb617e90fc9c4ececae329 (patch) | |
| tree | 4001a39072740a5be5b24533c05c1fe449906469 /plugins | |
| parent | 829238f2fe74c782023989e1871e15411b3e4ada (diff) | |
Generalisation of the "end command" argument of the goal printer.
This is meant to help integrate the printers of the declarative mode.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions