summaryrefslogtreecommitdiff
path: root/stdlib/gc.ml
diff options
context:
space:
mode:
authorJacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>2020-01-10 15:51:03 +0100
committerJacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>2020-01-11 13:19:10 +0100
commit0c8416478caa8cfdb7188384984d6c47782a7de9 (patch)
treef468af205dbf9303971963fca4d4178928d5368d /stdlib/gc.ml
parent8a79f6ce59cdabd65870af5124e3e3eebc366ff1 (diff)
downloadocaml-0c8416478caa8cfdb7188384984d6c47782a7de9.tar.gz
Drop support for tags in memprof.
They are somewhat difficult to handle for native allocations, and it is not clear how useful they are. Moreover, they are easy to add back since [Gc.Memprof.allocation] is a private record.
Diffstat (limited to 'stdlib/gc.ml')
-rw-r--r--stdlib/gc.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/stdlib/gc.ml b/stdlib/gc.ml
index 4b418d9fa0..18bade716f 100644
--- a/stdlib/gc.ml
+++ b/stdlib/gc.ml
@@ -124,7 +124,6 @@ module Memprof =
type allocation =
{ n_samples : int;
size : int;
- tag : int;
unmarshalled : bool;
callstack : Printexc.raw_backtrace }