indeed, last time I asked here it was not possible. For these tutorials I did a small hack to copy the images into the odoc dir, but I don’t know how to tell the ‘central docs’ to run this (make images)
indeed, last time I asked here it was not possible. For these tutorials I did a small hack to copy the images into the odoc dir, but I don’t know how to tell the ‘central docs’ to run this (make images)