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