/* Dummy version of set_std_prefix (needed by osint.adb) */

void
set_std_prefix (char *path, int len)
{
}

/* Dummy version of update_path (needed by osint.adb) */

char *
update_path (char *path, char *key)
{
  return path;
}