aboutsummaryrefslogtreecommitdiff
path: root/src/Rewriter.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-02-01 15:34:52 -0500
committerGravatar Jason Gross <jasongross9@gmail.com>2019-02-01 23:40:00 -0500
commit014c627a93f09c2867e76e35837eb8cb64f98384 (patch)
treeaf805d4456016fa598ea0a79eea51c61a351e3db /src/Rewriter.v
parent90c59282be5ba1f2cd7c2561d17f0559c140c597 (diff)
Improve travis stages
We combine two stages that are both fairly quick (early and lite), and we move nobigmem from coq to pre-standalone in an attempt to hopefully decrease the incidence of OOM issues on travis.
Diffstat (limited to 'src/Rewriter.v')
0 files changed, 0 insertions, 0 deletions