Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
more helpful error message with incompatible .cmis #3662
Original bug ID: 3662
Full_Name: henri dubois-ferriere
i just upgraded to 3.08.3, and by mistake did a 'make' in a directory which had
the error message was "misc.mli is not a compiled interface"
it would be good (esp for beginners who might get confused) if the error message