equal
deleted
inserted
replaced
95 |
95 |
96 /** build_history **/ |
96 /** build_history **/ |
97 |
97 |
98 private val default_rev = "tip" |
98 private val default_rev = "tip" |
99 private val default_multicore = (1, 1) |
99 private val default_multicore = (1, 1) |
100 private val default_heap = 1000 |
100 private val default_heap = 1500 |
101 private val default_isabelle_identifier = "build_history" |
101 private val default_isabelle_identifier = "build_history" |
102 |
102 |
103 def build_history( |
103 def build_history( |
104 hg: Mercurial.Repository, |
104 hg: Mercurial.Repository, |
105 progress: Progress = Ignore_Progress, |
105 progress: Progress = Ignore_Progress, |