[Demexp-dev] Re: [cduce-users] Problem while using cduce --mlstub

2005-07-15 Thread Thomas Petazzoni

Hello,

Alain Frisch wrote:


I guess the problem comes from different behaviors between shells (they
can put whatever they want in argv[0]). The next version of CDuce will
get rid of the external tool.


Okay, thanks. Will the other external tool mlcduce_wrapper disappear in 
next version ?


Currently, CDuce intalls these externals tools in /usr/bin, but Debian 
policy doesn't like undocumented binaries in /usr/bin. Debian wants 
either man-documented binaries in /usr/bin, or private undocumented 
tools in /usr/lib//. To correctly package the current 
version of the CDuce, I would have to hack it to that I can move cdo2ml 
and mlcduce_wrapper to /usr/lib/cduce/. So, if these tools are going to 
disappear soon, I think I'll wait for the next version ;-)


Sincerly,

Thomas
--
Thomas Petazzoni
[EMAIL PROTECTED]


___
Demexp-dev mailing list
Demexp-dev@nongnu.org
http://lists.nongnu.org/mailman/listinfo/demexp-dev


[Demexp-dev] Re: [cduce-users] Problem while using cduce --mlstub

2005-07-15 Thread Alain Frisch
Thomas Petazzoni wrote:
> Is it a bug ? Did I miss something ?

I guess the problem comes from different behaviors between shells (they
can put whatever they want in argv[0]). The next version of CDuce will
get rid of the external tool.

-- Alain


___
Demexp-dev mailing list
Demexp-dev@nongnu.org
http://lists.nongnu.org/mailman/listinfo/demexp-dev