- echo " $(INSTALL_DATA) '$$file' '$(prefix)/doc/simgrid/$$file'";\
- $(INSTALL_DATA) $$file $(prefix)/doc/simgrid/$$file ;\
+ echo " $(INSTALL_DATA) '$$file' '$(DESTDIR)/$(prefix)/doc/simgrid/$$file'";\
+ $(INSTALL_DATA) $$file $(DESTDIR)/$(prefix)/doc/simgrid/$$file ;\