aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2015-10-28 14:07:05 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2015-10-28 14:07:05 -0400
commitcdae9d225576146dc88902a466173170ee7e9dc1 (patch)
tree4db1f11eede0adddbb7bce490e6a664d45dd1730 /.gitignore
parentd655b90707449b7ebb2aa661fef6d947d9d88c58 (diff)
Tiny module-system tweaks in PointFormats
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
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
*~