| Commit message (Collapse) | Author | Age |
|\
| |
| |
| | |
wrongly tagged as keywords
|
| | |
|
| | |
|
| | |
|
| | |
|
|/
|
|
|
|
|
| |
One file was already ready for testing. We add another one.
Note that we have to remove the machine-dependent lines in the output
tex files.
|
|
|
|
|
|
|
| |
It drops anything after a `/`, so we change all `/`s into `.`.
There must be a better way to do this that doesn't involve so much bash
hackery, right?
|
| |
|
|\ |
|
|\ \ |
|
| | | |
|
| |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
There was an extra trailing space in #680.
Now things display as, e.g.,
```
TEST bugs/opened/3754.v
TEST bugs/opened/4803.v (-compat 8.4)
```
instead of
```
TEST bugs/opened/3754.v ( )
TEST bugs/opened/4803.v (-compat 8.4 )
```
|
|/
|
|
| |
We only want an absolute path, no need to follow symlinks.
|
|\ |
|
| | |
|
|/ |
|
| |
|
| |
|
|
|
|
|
|
|
| |
Was working when calling test-suite from main Makefile but not when
calling directly from the test-suite Makefile.
The dependency was mistakenly dropped in 98a927aef.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The rule is that any file misc/*.sh will now be automatically executed
from the test-file directory with appropriate environment variables
set. The test can use any auxiliary material which is put in a
directory of the same name as the test.
This avoids making the main Makefile more or more complex.
We loose some customization though (no more custom messages such as
printing of the number of universes in the test about the number of
necessary universes). We could preserve such customization if needed
but I did not consider it was worth the effort.
Warning: specific targets universes, deps-order, deps-checksum are
removed by consistency. Do instead "make misc/universes.log", etc., or
even "make misc" for all.
|
| |
|
| |
|
| |
|
|
|
|
| |
+ a few improvements on 5f1dd4c40 (lexing of { and }).
|
|\ |
|
| | |
|
| |
| |
| |
| | |
Order of items made stable
|
|\ \
| | |
| | |
| | | |
Was PR#303: LtacProf cutoff is for total percent, not time
|
|\ \ \
| | | |
| | | |
| | | | |
Was PR#302: Set the default LtacProf cutoff to 2%
|
| | | | |
|
| | | | |
|
| |/ /
|/| | |
|
|/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This was the original value from Tobias' code. When a user passes
-profile-ltac on the command line, or inserts [Show Ltac Profile] in the
document, the most useful default behavior is to not overload them with
useless information. When GUI clients want to display fancier profiling
information, there is no cost to the user to requiring them to specify
what cutoff they want. If the GUI client does not have any special
LtacProf handling, the most useful presentation is again the one that
cuts off the display at 2% total time.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| | |
Uses sed 's/\s*[0-9]*\.[0-9]\+\s*//g' and 's/\s*0\.\s*//g' to strip
numbers of seconds and to strip percentages. (This can potentially be
extended later.)
Add a test-suite file to make sure that LtacProf outputs some table.
|
| |
| |
| |
| |
| | |
This required improving the machinery of the test-suite Makefile to
support -compile.
|
|\| |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| | |
with a more explicit message.
|
|\| |
|
| | |
|
|\| |
|
| | |
|
|/ |
|
|
|
|
| |
Prop < Set < i for every global univ i
|
| |
|