diff options
| author | Prashanth Mundkur | 2018-04-18 17:14:32 -0700 |
|---|---|---|
| committer | Prashanth Mundkur | 2018-04-18 17:14:32 -0700 |
| commit | 70d7d17a1ffe0b4ca58a0c65792a48e4232d432f (patch) | |
| tree | 32027d28b894974af41f044317212cb97929f30d /src/state.ml | |
| parent | ae7fbb4ce5f5e52ec39ca17b152db63bbd0cfc69 (diff) | |
Remove obsolete comment.
Diffstat (limited to 'src/state.ml')
0 files changed, 0 insertions, 0 deletions