+# See .bashrc: export GDBHISTFILE="$HOME/.gdb_history"
+# Should also work <jefyi6bzm6.fsf@sykes.suse.de> (untested):
+# set history filename ~/.gdb_history
+set history save on
+# https://bugzilla.redhat.com/bugzilla/show_bug.cgi?id=106814
+set complaints 0
+set record insn-number-max 10000000
+define javadump
+ call _Jv_DeepDebug($arg0)
+end
+document javadump
+call _Jv_DeepDebug($arg0)
+end
+define pglist