diff options
| author | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-27 14:36:30 +0200 |
| commit | 53fb4203b80da48e2ac9b06803c57e81df702a0a (patch) | |
| tree | 0dc2a8efe8012190fcfcda50faf65365e30a3bad /lib/flags.ml | |
| parent | c65a1637b5e6cb60222963f29fc7c01bd7d1ee0b (diff) | |
| parent | 285bd0778bfa829e1969598cccd5d7c504d5fa90 (diff) | |
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.univ_print
Diffstat (limited to 'lib/flags.ml')
| -rw-r--r-- | lib/flags.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 8491873e07..2a1c50f52b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -60,7 +60,6 @@ let profile = false let ide_slave = ref false let raw_print = ref false -let univ_print = ref false let we_are_parsing = ref false |