Merge pull request #74680 from anmonteiro/anmonteiro/fix-kitty-0.15-patch

kitty: Fix patch that doesn't apply in v0.15.0
This commit is contained in:
Maximilian Bosch 2019-11-29 22:52:19 +01:00 committed by GitHub
commit 05aff9a635
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -1,11 +1,11 @@
--- a/setup.py
+++ b/setup.py
@@ -212,7 +212,7 @@
@@ -217,7 +217,7 @@ def init_env(
cflags = os.environ.get(
'OVERRIDE_CFLAGS', (
'-Wextra -Wno-missing-field-initializers -Wall -Wstrict-prototypes -std=c11'
'-Wextra {} -Wno-missing-field-initializers -Wall -Wstrict-prototypes -std={}11'
- ' -pedantic-errors -Werror {} {} -fwrapv {} {} -pipe {} -fvisibility=hidden'
+ ' {} {} -fwrapv {} {} -pipe {} -fvisibility=hidden'
).format(
float_conversion, std,
optimize,
' '.join(sanitize_args),