diff options
| author | Guillaume Melquiond | 2015-10-28 12:49:03 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-10-28 12:49:03 +0100 |
| commit | 1235c6c3cfc6770920f46de30b1c4b0f5cb44b19 (patch) | |
| tree | 573e563323a2218cc7f4739917da0feedc0f5094 /dev | |
| parent | ed7af646f2e486b7e96812ba2335e644756b70fd (diff) | |
Do not pause globing in funind. (Fix bug #4382)
Since the functions of this plugin exit by raising exceptions, globing
was never restarted. This prevented coqdoc from generating a proper
output whenever some feature of this plugin was used. There does not seem
to be any parsing of dynamic expressions, so pausing globing does not make
much sense in the first place.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions