OILS / devtools / gdbgui.sh View on Github | oilshell.org

52 lines, 15 significant
1#!/usr/bin/env bash
2#
3# Usage:
4# ./gdbgui.sh <function name>
5
6set -o nounset
7set -o pipefail
8set -o errexit
9
10# This leads to a Python 2/3 problem! Need pipx.
11bare_install() {
12 pip install gdbgui
13}
14
15# https://www.gdbgui.com/installation/
16
17install-pipx() {
18 python3 -m pip install --user pipx
19
20 # This modifies ~/.bash_profile, gah
21 #python3 -m userpath append ~/.local/bin
22}
23
24install() {
25 ~/.local/bin/pipx install gdbgui
26}
27
28run() {
29 ~/.local/bin/pipx run gdbgui
30}
31
32# Not working!
33#
34# No gdb response received after 10 seconds.
35#
36# Possible reasons include:
37# 1) gdbgui, gdb, or the debugged process is not running.
38
39# 2) gdb or the inferior process is busy running and needs to be interrupted
40# (press the pause button up top).
41
42# 3) Something is just taking a long time to finish and respond back to this
43# browser window, in which case you can just keep waiting.
44
45
46# TODO: Try this.
47#
48# Rename to devtools/debugger.sh
49
50# https://github.com/VSCodium/vscodium/releases
51
52"$@"