/* In general, we can't use the builtin `basename' function if available,
since it has different meanings in different environments.
/* In general, we can't use the builtin `basename' function if available,
since it has different meanings in different environments.