remove DEVELOPER_ROOT and PRODUCTION_ROOT, just guess ROOT from where this is installed
authorThierry Parmentelat <thierry.parmentelat@inria.fr>
Tue, 7 May 2013 07:14:02 +0000 (09:14 +0200)
committerThierry Parmentelat <thierry.parmentelat@inria.fr>
Tue, 7 May 2013 07:37:54 +0000 (09:37 +0200)

No differences found