diff options
Diffstat (limited to 'tools')
-rwxr-xr-x | tools/scripts/take_snapshot.py | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/scripts/take_snapshot.py b/tools/scripts/take_snapshot.py index 206c50ffc..3db3bac6c 100755 --- a/tools/scripts/take_snapshot.py +++ b/tools/scripts/take_snapshot.py @@ -313,6 +313,12 @@ if not commandNotFound: if commandNotFound or dos2unixVersion < StrictVersion('6.0.6'): raise Exception("You need dos2unix version 6.0.6 minimum.") +os.chdir(third_party) +ignore_case_setting = subprocess.Popen(['git', 'config', '--get', 'core.ignorecase'], stdout=subprocess.PIPE).communicate()[0] +if 'true' in ignore_case_setting: + raise Exception("Your 3rdparty repository is configured to ignore case. " + "A snapshot created with these settings would cause problems on case sensitive file systems.") + clearDirectory(third_party) exportNinja() |