...

An afterthought: you have defined in src/makefile.dj2 the variable DJDIRdos: it will probably do (and be valid for older djgpp versions) instead of /dev/env/DJDIR

That's the best approach I think. so after all we have

copy ..\doc\grx*um.inf $(DJDIRdos)\info\grx.inf install-info -e "* grx: (grx). GRAPHICS" \ $(DJDIRdos)\info\grx.inf $(DJDIRdos)\info\dir

if exist $(DJDIRdos)\info\grx.inf del -f $(DJDIRdos)\info\grx.inf install-info -r $(DJDIRdos)\info\grx.inf $(DJDIRdos)\info\dir

Ok, thanks. I will do that (without the -f of course).