projects
/
Faustine.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Merge branch 'master' of https://scm.cri.ensmp.fr/git/Faustine
[Faustine.git]
/
interpretor
/
main.ml
diff --git
a/interpretor/main.ml
b/interpretor/main.ml
index
8637875
..
21c2a8e
100644
(file)
--- a/
interpretor/main.ml
+++ b/
interpretor/main.ml
@@
-21,11
+21,11
@@
let set_GC () =
let _ = Gc.set { (Gc.get())
with Gc.space_overhead = 100 } in
let _ = Gc.set { (Gc.get())
let _ = Gc.set { (Gc.get())
with Gc.space_overhead = 100 } in
let _ = Gc.set { (Gc.get())
- with Gc.max_overhead = 0xFFF
FF
} in
+ with Gc.max_overhead = 0xFFF } in
let _ = Gc.set { (Gc.get())
with Gc.stack_limit = 0xFFFFF } in
let _ = Gc.set { (Gc.get())
let _ = Gc.set { (Gc.get())
with Gc.stack_limit = 0xFFFFF } in
let _ = Gc.set { (Gc.get())
- with Gc.allocation_policy =
0
} in
+ with Gc.allocation_policy =
1
} in
() ;;
let path_dsp = ref "";;
() ;;
let path_dsp = ref "";;