diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-13 14:07:13 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-03-13 14:07:13 +0100 |
commit | a50902cad6765f80fc394d08054a8516febf7600 (patch) | |
tree | 9ef82587e509df22e9bd46b82d7bb9de79d379ff /backend/PrintXTL.ml | |
parent | 4d7a6709946a0c30e932c00405252b42e348eb64 (diff) | |
download | compcert-a50902cad6765f80fc394d08054a8516febf7600.tar.gz compcert-a50902cad6765f80fc394d08054a8516febf7600.zip |
Anchor patterns to the top-level directory when appropriate
It's OK to ignore *.o in any directory, but it's safer to ignore
"/ccomp" (ccomp in the top-level directory) than to ignore
"ccomp" (ccomp in any directory).
Diffstat (limited to 'backend/PrintXTL.ml')
0 files changed, 0 insertions, 0 deletions