diff options
author | Adam Chlipala <adam@chlipala.net> | 2015-10-28 14:07:05 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2015-10-28 14:07:05 -0400 |
commit | cdae9d225576146dc88902a466173170ee7e9dc1 (patch) | |
tree | 4db1f11eede0adddbb7bce490e6a664d45dd1730 /.gitignore | |
parent | d655b90707449b7ebb2aa661fef6d947d9d88c58 (diff) |
Tiny module-system tweaks in PointFormats
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index ae784f4a5..cec91e9a6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ +bedrock fiat *~ |