Anonymous committed f47fdf0

PR#5278: update Makefile message to mention "make world.opt"


  • Participants
  • Parent commits f2d328d

Comments (0)

Files changed (1)

 	@echo "Please refer to the installation instructions in file INSTALL."
 	@echo "If you've just unpacked the distribution, something like"
 	@echo "	./configure"
-	@echo "	make world"
-	@echo "	make opt"
+	@echo "	make world.opt"
 	@echo "	make install"
 	@echo "should work.  But see the file INSTALL for more details."