feature request: allow code on stdin for gcc compat

[didickman]

In my build system, gcc takes input from stdin like below. It would be nice if CompCert allowed the same thing.

Of course, the code on my end can be easily rewritten if needed...

$ printf '#include <paths.h>\n_PATH_STDPATH\n' |  gcc -E -P  -
"/usr/bin:/bin:/usr/sbin:/sbin:/usr/X11R6/bin:/usr/local/bin"

$ printf '#include <paths.h>\n_PATH_STDPATH\n' |  ccomp -E -P  -
Unknown argument `-'

[bschommer]

If we include the -pipe option we can have a look into including this.

[didickman]

The pipe option would be useful too (at the moment I have a custom patch to just ignore the pipe flag when it’s used from various system makefiles). That being said it’s been a few years since I opened this PR and it can be worked around outside of compcert as I point out above. Therefore perhaps another candidate to consider closing?