diff options
author | Eelco Dolstra <edolstra@gmail.com> | 2019-11-08 16:23:57 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-08 16:23:57 +0100 |
commit | d1db7fa9528154284de55d37e5186ac06fcbffc9 (patch) | |
tree | d89efde5e36c4ece00153e5aad38fad7f06f4977 /src/libexpr/names.hh | |
parent | 0d6774468cf109c9cb6502cb81f1219c6e68ee37 (diff) | |
parent | a08f35392256b1ef23947857e41a9b12b1591245 (diff) |
Merge pull request #3211 from zimbatm/gitignore-precompiled-headers
gitignore /precompiled-headers.h.gch
Diffstat (limited to 'src/libexpr/names.hh')
0 files changed, 0 insertions, 0 deletions