Actually, we may want to ask Werner. He's an expert on csh. @Werner, could you have a look if there is a better fix for this? You will find the corresponding change for bash there as well.