Open nojb opened 3 months ago
This is because on Windows it is common for %%LIBDIR%% in
%%LIBDIR%%
https://github.com/dbuenzli/down/blob/e3a4f38e02bf75fd0206d97dc74c6a5c26342023/src/down.top#L9
to contain backslashes, which need to be escaped (eg by using String.escaped) in
String.escaped
https://github.com/dbuenzli/down/blob/e3a4f38e02bf75fd0206d97dc74c6a5c26342023/pkg/pkg.ml#L20
Isn't it rather the #directory directive implementation which should escape ?
#directory
Forget about that.
This is because on Windows it is common for
%%LIBDIR%%
inhttps://github.com/dbuenzli/down/blob/e3a4f38e02bf75fd0206d97dc74c6a5c26342023/src/down.top#L9
to contain backslashes, which need to be escaped (eg by using
String.escaped
) inhttps://github.com/dbuenzli/down/blob/e3a4f38e02bf75fd0206d97dc74c6a5c26342023/pkg/pkg.ml#L20