MPS issue job003533

TitleIt's not clear what's the best way to build the MPS
Assigned userGareth Rees
DescriptionChristian Schafmeister wrote in #memorypoolsystem: "When I configure MPS with "configure" it says: CONFIGURE/MAKE IS NOT THE BEST WAY TO BUILD THE MPS -- see <manual/build.txt>" But manual/build.txt seems to indicate that configure/make is a good way to build MPS - any tips on the best way to install it?"
AnalysisThere is no contradiction here: something can be "good" and yet "not the best". However, perhaps the documentation could be improved -- an explicit discussion of the different ways of building the MPS and the trade-offs involved might be helpful to a puzzled beginner.
How foundcustomer
EvidenceSee text quoted from #memorypoolsystem
Observed in1.111.0
Created byGareth Rees
Created on2013-07-01 13:27:40
Last modified byGareth Rees
Last modified on2014-04-15 11:13:55
History2013-07-01 GDR Created.


Change Effect Date User Description
185544 closed 2014-04-15 11:13:54 Gareth Rees Be clearer in the output of configure that configure/make is one way to build the MPS, but alternative approaches may be better.