On 15/12/2017 18:41, Makarius wrote:
On 15/12/17 17:46, David Matthews wrote:
On 15/12/2017 16:15, Makarius wrote:
* The polyc script cannot handle directory names with spaces, e.g. the
main "prefix".
I guess it would need some extra quotation. Do you want to propose a fix?
See the included change: my very first commit produced with git (with
VSCode and gitk).
Thanks. I've merged and pushed it.
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
