#!/bin/sh

SHELL=/bin/sh script --flush --quiet --return /var/tmp/workbench --command "re.sonny.Workbench $@"
# SHELL=/bin/sh script --flush --quiet --return /var/tmp/workbench --command "G_MESSAGES_DEBUG=\"re.sonny.Workbench\" re.sonny.Workbench $@"
