GitLab

This fixes #427.

We do this by tacking on a tilde if # is followed by a digit, to prevent it
from being mistaken for a $ substitution (which happens because $ becomes # in
FUDI, which is required behavior by non-iem gui objects and thus we don't want
to break this). The tilde gets removed automatically when the label is sent to
the gui.

All this is implemented using the existing symbol mungers in the
iemgui_dollar2raute and iemgui_raute2dollar functions in g_all_guis.c and
iemgui_escape and iemgui_unescape in dialog_iemgui.html.

Help browser: Cosmetic changes in the GUI prefs, add a warning about the impact of help browser settings on startup times.

Help browser: Move the index construction into pdgui.js, so that it is only done once during startup.

Help browser: Construct the help index from all of lib/pd-l2ork, to make the keyword search more useful.

Fix up the install/uninstall targets to properly handle the case that the build directory doesn't exist.

Add convenience targets to the toplevel Makefile which install additional abstractions and externals after a light build. E.g.: make light pdlua_ext