--- /dev/null
+--- bash-5.0/examples/loadables/push.c~ 2017-06-20 16:54:52.000000000 +0200
++++ bash-5.0/examples/loadables/push.c 2019-03-21 14:40:08.789376401 +0100
+@@ -36,7 +36,7 @@ extern int errno;
+ #endif
+
+ extern int dollar_dollar_pid;
+-extern int last_command_exit_value;
++extern volatile int last_command_exit_value;
+
+ int
+ push_builtin (list)