| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Work done by Assia Mahboubi and Enrico Tassi
|
|
We make it so that, by default, the HTML reference manual looks
like the one published online (same .css) and we provide a target
to serve it locally (requires python).
|
|
This is a followup of 7d1fc15. Without this fix, you're warned of leftover files,
but even a 'make clean' is then refused, so you cannot get rid of them easily
(apart via a git clean -xfd).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
y , z".
|
|
|
|
|
|
|
|
|
|
As suggested by @herbelin.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also includes a minor fix of the Extraction doc (a Require was missing).
|
|
|
|
Minor clean up, no sense in having these as they do nothing.
|
|
It is empty and not used anymore.
|
|
|
|
|
|
|
|
|
|
|
|
TestCompile)
|
|
|
|
|
|
|
|
4844 and 4824)
|
|
|
