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

[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/<packagename>/. 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
address@hidden