summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-01-30 20:21:15 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-01-30 20:21:15 -0500
commitb194870eb8f62e858d9fd36d72655f99a60e0b11 (patch)
treedbd0ace7dff0a6991ebab35dca559a7e13810d51
parent90dd3a368654d5839d37fb5afdc0bf1599052a6b (diff)
Remove unneeded lib/c directory
-rw-r--r--lib/c/.dir0
1 files changed, 0 insertions, 0 deletions
diff --git a/lib/c/.dir b/lib/c/.dir
deleted file mode 100644
index e69de29b..00000000
--- a/lib/c/.dir
+++ /dev/null