diff options
| author | Brian Campbell | 2021-02-25 15:01:43 +0000 |
|---|---|---|
| committer | Brian Campbell | 2021-02-25 15:01:43 +0000 |
| commit | ace7b32fe420234575ad7564f64c76309e3a74b3 (patch) | |
| tree | 08d07586ee8199dceff9d0ab77fc453008118f9e /src/jib/jib_util.ml | |
| parent | bb0a81f2170d068f561c6380bff500d568a7ffd3 (diff) | |
Remove accidental use of too-recent Option module
Also drop a related bit of dead code
Diffstat (limited to 'src/jib/jib_util.ml')
0 files changed, 0 insertions, 0 deletions