--include-dependencies, -d not recognised by jenkins-cheri-build.py?

[khilangudka]

This works fine with cheribuild.py but gives the following error with jenkins-cheri-build.py:

jenkins-cheri-build.py: error: unrecognized arguments: -d

[arichardson]

I think I explitly disabled it for the Jenkins version to ensure that we don't accidentally build other projects. I guess I could change that.

[khilangudka]

I think for the short term it would be useful for webkit because of all the dependencies. It's much easier just to build it with -d. In the long term we should ideally have all dependencies as separate projects and run their respective test suites.

[khilangudka]

Actually thinking about it... we could just individually build the dependencies in the webkit jenkins job so I think we can ignore needing -d if this is the only case it would be useful.