# HG changeset patch
# User Eli Zaretskii <eliz@gnu.org>
# Date 965730931 0
# Node ID d8bdb143d14006483484ddd84630c55850420609
# Parent  321084a896d12fdb01ede07c637cf342ad0bc2b7
(maindir): Update src/_gdbinit even if it does already exist.

diff -r 321084a896d1 -r d8bdb143d140 config.bat
--- 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