1
0
mirror of https://github.com/MariaDB/server.git synced 2025-07-30 16:24:05 +03:00
Docs/manual.texi:
  Auto merged
This commit is contained in:
unknown
2001-12-13 02:38:39 +02:00
5 changed files with 257 additions and 78 deletions

View File

@ -263,10 +263,9 @@ while test $# -gt 0; do
$ECHO "Note: you will get more meaningful output on a source distribution compiled with debugging option when running tests with --gdb option"
fi
DO_GDB=1
# We must use manager, as things doesn't work on Linux without it
# This needs to be checked properly
# USE_MANAGER=1
# USE_RUNNING_SERVER=""
USE_RUNNING_SERVER=""
;;
--client-gdb )
if [ x$BINARY_DIST = x1 ] ; then