diff options
| author | Daniel Narvaez <dwnarvaez@gmail.com> | 2012-12-15 09:39:22 (GMT) |
|---|---|---|
| committer | Daniel Narvaez <dwnarvaez@gmail.com> | 2012-12-15 09:39:22 (GMT) |
| commit | 6d24aa66ebb5231ead47bf5f0924908b76acd622 (patch) | |
| tree | 536ca5495a88f1f45ead98aa97aadf192a3f7072 /devbot/config.py | |
| parent | 33d8978886a6b5e610367e24331bce79be8cd08c (diff) | |
Put real_prefix_path in the home
So that it doesn't get deleted when we clean. Otherwise every time
the prefix is different and ccache is useless.
Diffstat (limited to 'devbot/config.py')
| -rw-r--r-- | devbot/config.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/devbot/config.py b/devbot/config.py index a6d2b49..31abe3d 100644 --- a/devbot/config.py +++ b/devbot/config.py @@ -121,7 +121,7 @@ def _setup_home_dir(dir): def _setup_prefix_dir(dir, relocatable): global prefix_dir - real_prefix_path = os.path.join(dir, "real_prefix") + real_prefix_path = os.path.join(config_home_dir, "real_prefix") if os.path.exists(real_prefix_path): with open(real_prefix_path) as f: |