Dear Eliseo, Many thanks for the information.
Is it correct that the version of sed you are using is not GNU sed? In that case, would it be possible for you to try installing gnu sed, please? Once it's done and you are sure that simply running sed runs gnu SED, can you please make a make distclean ./configure make and see whether that works? Thanks, Sébastien. _______________________________________________ Cocci mailing list [email protected] https://systeme.lip6.fr/mailman/listinfo/cocci
