17 Nov
2004
17 Nov
'04
10:40 a.m.
Just make sure you agree with whomever invented the "module.pmod.in as directory" feature what the intended behaviour is. What you suggested looks OK to me, but I've never used that feature...
If make generates module.pmod/module.pmod instead of the normal module.pmod (why?), it probably would make sense to have it generate module.pmod/__Foo.so as well.