changeset 30657:d8bdb143d140

(maindir): Update src/_gdbinit even if it does already exist.
author Eli Zaretskii <eliz@gnu.org>
date Tue, 08 Aug 2000 10:35:31 +0000
parents 321084a896d1
children 7ddcabbcb378
files config.bat
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/config.bat	Tue Aug 08 01:39:26 2000 +0000
+++ b/config.bat	Tue Aug 08 10:35:31 2000 +0000
@@ -219,7 +219,7 @@
 Echo Configuring the main directory...
 If "%DJGPP_VER%" == "1" goto mainv1
 Echo Looking for the GDB init file...
-If not Exist src\_gdbinit If Exist src\.gdbinit update src/.gdbinit src/_gdbinit
+If Exist src\.gdbinit update src/.gdbinit src/_gdbinit
 If Exist src\_gdbinit goto gdbinitOk
 Echo ERROR:
 Echo I cannot find the GDB init file.  It was called ".gdbinit" in