diff options
| author | hallgren <hallgren@chalmers.se> | 2013-12-10 16:49:40 +0000 |
|---|---|---|
| committer | hallgren <hallgren@chalmers.se> | 2013-12-10 16:49:40 +0000 |
| commit | dd1b474a22011475fb47623f28715105d8805f22 (patch) | |
| tree | 104bae310715fab0060e7b559c034b69302f8495 /src/ui | |
| parent | 0851308099f625bb451f80e62e33137df199322f (diff) | |
testsuite: fix test of generate_trees
There were two differences between the current output and the old gold file:
1. The trees are no longer generated with increasing depth
2. The meaning of the -depth flag has changed: for example,
"gt -cat=Nat -depth=1" used to generate only "zero",
now you also get "succ zero".
Diffstat (limited to 'src/ui')
0 files changed, 0 insertions, 0 deletions