-
Sylvain Dailler authored
We want to use Glob outside of why3doc to associate locations to ident (original locations for Find_ident_req). We need to allow glob to be erased on a per file basis to: - avoid consuming too much memory, - avoid having obsolete location information still saved in glob
1dcc51cb