From 609c74133dd867350fcd3946ed2912ae91e993c9 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Fri, 5 Sep 2008 14:50:11 -0700
Subject: Add a .gitignore file to ignore "dist" directories.

---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 .gitignore

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..9b1c8b1
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/dist
-- 
cgit v1.2.3