On 2 juil. 2012, at 10:35, Adrien wrote: > Hi, > > A couple of random ideas. > > One possible way is to install godi in /opt/godi everywhere. > > Another variation is to install it in /, move it inside $HOME/godi and > when there is a need to update files, chroot to $HOME/godi (possibly > with --userspec set) and update that way. It's not terribly sexy but > should be simple and reliable.
Thanks. These are interesting options as well. Alan _______________________________________________ Godi-list mailing list Godi-list@ocaml-programming.de https://godirepo.camlcity.org/mailman/listinfo/godi-list