On Tue, Apr 9, 2024, at 11:35 PM, Jacob Bachmeyer wrote: > Jan Engelhardt wrote: >> On Tuesday 2024-04-09 05:37, Jacob Bachmeyer wrote: >> >>>> In principle it could be posible to output something different to >>>> describe this stramge situation explicitly. For instance, output >>>> "via stdin" as a comment, or output `stdin/../filename' as the file >>>> name. (Programs that optimize the file name by deleting XXX/.../ >>>> are likely not to check whether XXX is a real directory.) ...
How about `/dev/stdin/-` if no filename has been specified with #line or whatever, and `/dev/stdin/[filename]` if one has, where [filename] is the specified filename with all leading dots and slashes stripped, falling back to `-` if empty? /dev/stdin can be relied on to either not exist or not be a directory, so these shouldn't ever be openable. zw
