[gedit-list] External tools can't be stopped?

[Jef Driesen <jefdriesen hotmail com>]

Hi,

When I launch an external tool like the builtin make, and try to abort 
it with the stop button, it doesn't work. The shell output pane shows 
the message "Stopped. Exited: 15", but then it keeps running.

Is this a bug in gedit, or something in the script that is causing this?

Jef