Index: boot/Makefile
===================================================================
--- boot/Makefile	(revision 405b67c762b3d9e7646b77e3813c5ac9bfd3badd)
+++ boot/Makefile	(revision 7e9e652913a5985f37d6cd1f38ebc993db6a8849)
@@ -113,5 +113,5 @@
 		file_dir="`dirname "$$file"`" ; \
 		file_name="`basename "$$file"`" ; \
-		cp "$(USPACE_PATH)/$(DRVS_PATH)/$$file_dir/$$file_name/$$file_name.dev" "$(DIST_PATH)/$(DRVS_PATH)/$$file_name/" ; \
+		cp "$(USPACE_PATH)/$(DRVS_PATH)/$$file_dir/$$file_name/"*".dev" "$(DIST_PATH)/$(DRVS_PATH)/$$file_name/" ; \
 	done
 	for file in $(RD_DRVS_FW) ; do \
