/* Return the name of the executable file as a string.
ERR nonzero means get error if there is none specified;
otherwise return 0 in that case. */
-extern char *get_exec_file (int err);
+extern const char *get_exec_file (int err);
/* Return the inferior's current working directory. If nothing has
been set, then return NULL. */