+# (Note: remote-es.o is also available from the standard monitor.mt
+# configuration. The only difference in this configuration is that it
+# has its own DEFAULT_PROMPT and GDBINIT_FILENAME, if you don't care
+# about those things you can just use monitor.mt).