diff options
| author | Kazuhiko Sakaguchi | 2018-04-23 09:20:02 +0900 |
|---|---|---|
| committer | GitHub | 2018-04-23 09:20:02 +0900 |
| commit | 0900b007973759a0fea20c0395e40c6f34bed8dc (patch) | |
| tree | a9e95a528057a70a327916d9ca8e94507bc44f71 /kernel/uGraph.ml | |
| parent | dfbf22a098e8e2890d2e10da5d669d9960ef6771 (diff) | |
Fix a typo in the reference manual: <; -> <:
Diffstat (limited to 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions