File tree Expand file tree Collapse file tree 1 file changed +12
-6
lines changed
test/xref2/big_search_path.t Expand file tree Collapse file tree 1 file changed +12
-6
lines changed Original file line number Diff line number Diff line change 11We create a lot of directories
22
3- $ for ((i = 1; i <= 1000; i++)); do
4- > mkdir -p d$i
3+ $ i=1
4+ > while [ $i -le 1000 ]; do
5+ > mkdir -p d$i
6+ > i=$( (i + 1))
57 > done
68
79 $ echo " {0 Heading}" > p.mld
810
9- $ for ((i = 1; i <= 1000; i++)); do
10- > echo " {!Module$i }" >> p.mld
11+ $ i=1
12+ > while [ $i -le 1000 ]; do
13+ > echo " {!Module$i }" >> p.mld
14+ > i=$( (i + 1))
1115 > done
1216
1317 $ odoc compile p.mld
@@ -19,8 +23,10 @@ It should not take more than 0.1 seconds to link p!
1923Now let' s investigate another scenario: a single directory with many unrelated files.
2024
2125 $ mkdir -p one_dir
22- $ for ((i = 1; i <= 10000; i++)); do
23- > touch one_dir/file_$i
26+ $ i=1
27+ > while [ $i -le 1000 ]; do
28+ > touch one_dir/file_$i
29+ > i=$((i + 1))
2430 > done
2531
2632Should not take long to link:
You can’t perform that action at this time.
0 commit comments