Project

General

Profile

« Previous | Next » 

Revision 64385d42

Added by Pierre-Loïc Garoche almost 7 years ago

Turn an option to off by default: it was triggering scope plugin automatically

View differences:

src/plugins/scopes/scopes.ml
162 162

  
163 163
let option_show_scopes = ref false
164 164
let option_scopes = ref false
165
let option_all_scopes = ref true
165
let option_all_scopes = ref false
166 166
let option_mem_scopes = ref false
167 167
let option_input_scopes = ref false
168 168

  

Also available in: Unified diff