diff options
| author | Pierre-Marie Pédrot | 2014-08-24 19:28:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-08-24 19:54:16 +0200 |
| commit | ac1344e750395b26513d1ca963107f14e7d0f06f (patch) | |
| tree | 5a41c46ed388d12396c3c8de537f8cc15973c9c3 /doc/RecTutorial | |
| parent | c2bde259c207f9ff9cb199906879cd1e19a75ced (diff) | |
Enabling drag & drop on the source view widgets.
Sort of fixes bug #2765, but the file loading is broken and puts coqtop in
an inconsistent state, so that even the previous half-working patch was
actually not functionning at all. This should be fixed eventually.
Diffstat (limited to 'doc/RecTutorial')
0 files changed, 0 insertions, 0 deletions