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).
?? * Instead of insisting in hardwired directory locations it should be possible to refer to the relative location of the polyc itself.? In GNU bash I am using THIS="$(cd "$(dirname "$0")"; pwd)" -- it is unclear to me how to do it in /bin/sh.
The paths are set from the installation directories in configure i.e. where the binaries and libraries are to be installed.? It's possible to set the library and binary directories independently so there's no necessary relationship between them.
The above change might already be sufficient for that: isabelle build_polyml merely needs to change /bin/sh into bash and make the prefix relative. This will allow users of Isabelle to use the bundled Poly/ML polyc, even though it is not directly relevant for Isabelle -- see also https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-February/msg00144.h...
I see further references to the install dir in:
pkgconfig/polyml.pc libpolymain.la libpolyml.la
Are these relevant for polyc?
Makarius