mirror of
https://github.com/Mercury-Language/mercury.git
synced 2025-12-06 07:49:02 +00:00
More generally, clean-up the various batch files we have.
scripts/mdb.bat.in:
Ensure that the value of MERCURY_DEBUGGER_INIT environment variable does
*not* include double quotes, otherwise the path to the mdbrc file will
be incorrect.
scripts/*.bat.in:
Require command extensions to be enabled. This is the default on
all Windows systems we support; explicitly enabling them is just in case
the user turns them off for some reason.
Don't disable echoing twice.
Quote the entire argument to the set command; this should avoid double
quotes ending up where we don't want them.
Update copyright notices.
22 lines
831 B
Batchfile
22 lines
831 B
Batchfile
@echo off
|
|
rem @configure_input@
|
|
rem ---------------------------------------------------------------------------
|
|
rem Copyright (C) 2011 The University of Melbourne.
|
|
rem Copyright (C) 2020, 2024 The Mercury team.
|
|
rem This file may only be copied under the terms of the GNU General
|
|
rem Public License - see the file COPYING in the Mercury distribution.
|
|
rem ---------------------------------------------------------------------------
|
|
rem
|
|
rem mdb.bat - Mercury debugger
|
|
rem Usage: mdb [<options>] <executable> [<args>] ...
|
|
rem
|
|
rem ---------------------------------------------------------------------------
|
|
|
|
rem Do not export any local environment changes and ensure command extensions
|
|
rem are enabled.
|
|
setlocal enableextensions
|
|
|
|
set "MERCURY_OPTIONS=%MERCURY_OPTIONS% -Di"
|
|
set "MERCURY_DEBUGGER_INIT=@PREFIX@\lib\mercury\mdb\mdbrc"
|
|
%*
|