#!/bin/sh
argv0="$0"; shift; "$argv0"_"$0" "$@"
