Closed steve-cs closed 3 years ago
Commit https://github.com/AdaCore/gps/commit/1a90c16a1f7614cf43007a185fd96f0b949aa988 adds unused "when others => null;" causing development build to fail until we actually get new layers (presumably) in gtkada. I'll patch out that commit in gps-src for now.
[Ada] src_editor_view.adb src_editor_view.adb:1253:15: warning: "others" choice is redundant src_editor_view.adb:1253:15: warning: previous choices cover all values
Reverted upstream, commit https://github.com/AdaCore/gps/commit/c64ceaf055059cc1928a3a0fe1cb164e2ee3001b
Commit https://github.com/AdaCore/gps/commit/1a90c16a1f7614cf43007a185fd96f0b949aa988 adds unused "when others => null;" causing development build to fail until we actually get new layers (presumably) in gtkada. I'll patch out that commit in gps-src for now.