Repository navigation
feature request: allow code on stdin for gcc compat #166
Description
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 `-'
Activity
bschommer commentedon Feb 13, 2017
If we include the -pipe option we can have a look into including this.
didickman commentedon Oct 1, 2021
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?