From 018f16d30cf506879df06429582ebec27bb063ae Mon Sep 17 00:00:00 2001
From: Carl Eastlund <cce@racket-lang.org>
Date: Thu, 20 Sep 2012 12:08:22 -0400
Subject: [PATCH] Added $PLT/compiled-root/ to git's ignore list so we have
 somewhere convenient to point PLTCOMPILEDROOTS at.  This is much like
 $PLT/add-on/ for PLTADDONDIR and $PLT/house-calls/ for DrDr.

---
 .gitignore | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/.gitignore b/.gitignore
index abc8383fea..93613b4720 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,9 @@
 # a common convenient place to set the PLTADDON directory to
 /add-on/
 
+# a common convenient place to set the PLTCOMPILEDROOTS directory to
+/compiled-root/
+
 # location for cached DrDr report files
 /house-calls/