diff options
| author | Samuel Gruetter | 2017-11-06 12:08:49 -0500 |
|---|---|---|
| committer | Samuel Gruetter | 2017-11-06 12:08:49 -0500 |
| commit | b75e6f61d2828a1c4da41f919182dda551ea9d47 (patch) | |
| tree | 9ecf929421fa664b113998d9bc2c0706bee2d22c /kernel/declarations.ml | |
| parent | e029cf5b417b22ebc65a8193469bbbe450f725ce (diff) | |
Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",
not "first [ progress tac1 | progress tac2 ]".
And add a missing backslash.
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions