diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2016-10-17 10:10:25 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-10-17 10:10:25 +0200 |
| commit | bdce7eefa046c7b9520a5e243de11428b0e7ff2a (patch) | |
| tree | 5f8c480a64aa3cf450f812d5df49b607e7bfa0e5 /doc/tools/doc_merge.py | |
| parent | dccbd4aa6b9914fd275901537a3fc8e9e827ea7d (diff) | |
| parent | 4a57821349fc8fd4d4c7e375a1f8cf09623ee856 (diff) | |
Merge pull request #6846 from volzhs/android-dir-exists
Fix crash when using Directory.dir_exists(path) on Android
Diffstat (limited to 'doc/tools/doc_merge.py')
0 files changed, 0 insertions, 0 deletions