Files
mercury/scripts
Julien Fischer f7921d7b47 Fix a problem using mdb from cmd.exe on Windows.
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.
2024-01-12 18:19:21 +11:00
..
2020-06-27 15:06:21 +10:00
2023-09-07 11:47:38 +10:00
2023-09-07 11:47:38 +10:00
2023-09-22 23:13:22 +10:00