diff options
| author | Arnaud Spiwack | 2014-10-28 11:41:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-11-01 22:43:57 +0100 |
| commit | f68208495d83c670039a95b6b44809b263e43ef2 (patch) | |
| tree | e804c31ad0deb85cfc3f8f6e508014a787f357a1 /printing/printer.ml | |
| parent | 967883e29a46a0fff9da8e56974468531948b174 (diff) | |
Info: dispatching-branches are declared as such in the info trace.
Hence dispatches are printed as dispatches rather than sequences.
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions