1 Oct
2011
1 Oct
'11
3:01 a.m.
+ * 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.