diff options
| author | Rozelette <Rozelette@users.noreply.github.com> | 2020-09-13 20:09:13 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-13 21:09:13 -0400 |
| commit | ec912054dab3432515c78e1b548e96183238ab55 (patch) | |
| tree | 5d02604f05d42bbd769d8ca6b9dd2870a4897370 /diff_settings.py | |
| parent | 189d0d6c306ab7678bae1651ffd4d5a1dd6da977 (diff) | |
Update tools (#16)
* Clean up .gitignore
* Set exec bit on all python and shell scripts
* Delete unused files
* Add decomp-permuter repo
* Update submodules
Diffstat (limited to 'diff_settings.py')
| -rwxr-xr-x[-rw-r--r--] | diff_settings.py | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/diff_settings.py b/diff_settings.py index 784286ddc..784286ddc 100644..100755 --- a/diff_settings.py +++ b/diff_settings.py |