History log of /seL4-l4v-master/HOL4/tools/Holmake/tests/badincludes/selftest.sml
Revision Date Author Comments
# f860f0f1 24-Oct-2019 Michael Norrish <Michael.Norrish@nicta.com.au>

Fix a couple of Holmake tests

- In badincludes, the output being tested has changed to use an
absolute path instead of a relative path.
- In holdep, the dependency on the cmp.exe utility needs to be
explicitly mentioned (and this seems totally reasonable to me).
Previously, the system relied on the fact that it got built when the
INCLUDES was recursed into. Now Holmake won't build stuff in the
INCLUDES directories unless a target actually requires it.
- In testsrc, there is an analogous dependency on unicode-grep that
needs to be made explicit


# 902ac12a 29-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Make a Holmake test build under Moscow ML


# d37e96c6 25-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Proper version of c85433294

Still closes #572


# 89a1afdc 25-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Revert "Make Holmake report problems with INCLUDES/-I paths better"

This reverts commit c8543329459313ad015b9158e36841616d02d5e5.

My failed git skills around developing on multiple directories in
parallel dropped the previous commit.


# c8543329 25-Nov-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Make Holmake report problems with INCLUDES/-I paths better

Closes #572