Support dropping files over the coqide window. (Partial fix for bug #2765)

The fix is only partial, because dropping files only works over the menu
bar, the icon bar, the status bar, and so on. Editable boxes, such as the
script widget, catch dnd events, hence preventing this code from working
for these drop targets. Some (labl)gtk expert should be able to sort it
out.

0 files changed, 0 insertions, 0 deletions