summaryrefslogtreecommitdiff
path: root/platform/x11
diff options
context:
space:
mode:
authorRĂ©mi Verschelde <rverschelde@gmail.com>2018-01-26 21:25:20 +0100
committerGitHub <noreply@github.com>2018-01-26 21:25:20 +0100
commit88aed259f90c6f49e22f57a7eae6c2632010bccd (patch)
tree5b35afb4f115d108948c9fb59ebf24fd758ccb19 /platform/x11
parent9ba5fb87f009faea406e3968f4d88234752d635b (diff)
parentc6d9a7665acdd5785760eee0c69bd1d2a53b6b90 (diff)
Merge pull request #16092 from hpvb/make-separate-debug-symbols-opt-in
Make separate debug symbols opt-in
Diffstat (limited to 'platform/x11')
-rw-r--r--platform/x11/SCsub2
-rw-r--r--platform/x11/detect.py1
2 files changed, 2 insertions, 1 deletions
diff --git a/platform/x11/SCsub b/platform/x11/SCsub
index 38dd2ddd88..b18757337a 100644
--- a/platform/x11/SCsub
+++ b/platform/x11/SCsub
@@ -19,5 +19,5 @@ common_x11 = [
prog = env.add_program('#bin/godot', ['godot_x11.cpp'] + common_x11)
-if env["debug_symbols"] == "full" or env["debug_symbols"] == "yes":
+if (env["debug_symbols"] == "full" or env["debug_symbols"] == "yes") and env["separate_debug_symbols"]:
env.AddPostAction(prog, make_debug)
diff --git a/platform/x11/detect.py b/platform/x11/detect.py
index 5c8564376f..02bd7232c2 100644
--- a/platform/x11/detect.py
+++ b/platform/x11/detect.py
@@ -55,6 +55,7 @@ def get_opts():
BoolVariable('pulseaudio', 'Detect & use pulseaudio', True),
BoolVariable('udev', 'Use udev for gamepad connection callbacks', False),
EnumVariable('debug_symbols', 'Add debug symbols to release version', 'yes', ('yes', 'no', 'full')),
+ BoolVariable('separate_debug_symbols', 'Create a separate file with the debug symbols', False),
BoolVariable('touch', 'Enable touch events', True),
]