Alvaro Herrera <alvherre@commandprompt.com> writes:
> Excerpts from Aidan Van Dyk's message of sáb jul 07 11:32:33 -0400 2012:
>> But, since you're using operators, what would you think is an
>> appropriate name for the file the operator is dumped into?
> I was thinking that it might make sense to group operators according to
> the type(s) they operate on, somehow. Using funny chars for names is
> guaranteed to cause problems somewhere.
Sure. You need not look further than "/" to find an operator name that
absolutely *will* cause trouble if it's dumped into a filename
literally.
I'm not especially thrilled by the idea of using url-encoding or
something like that for operator names, though. Seems like it loses on
readability.
If we think that operators outside of extensions will be an infrequent
special case, what about just dumping all of them into a single file
named "operators"? And similarly for casts?
regards, tom lane