// the selection in the object browser.
// Note: processEvents() should be called after updateGV(),
// otherwise the application crashes from time to time.
// the selection in the object browser.
// Note: processEvents() should be called after updateGV(),
// otherwise the application crashes from time to time.