+ * We can't use the native f* functions because of the filename syntax differences + * between DOS and Unix. That doesn't belong in a function comment; it's an implementation detail that belongs, at most, inside the function.