remove an out of date comment

The mentioned todo was closed.

diff --git a/doc/profiling/comment_9_7e1a06690b52d241b2d57be0864d6f26._comment b/doc/profiling/comment_9_7e1a06690b52d241b2d57be0864d6f26._comment
deleted file mode 100644 (file)
index 3212ef1..0000000
--- a/doc/profiling/comment_9_7e1a06690b52d241b2d57be0864d6f26._comment
+++ /dev/null
@@ -1,18 +0,0 @@
-[[!comment format=mdwn
- username="joey"
- subject="""comment 9"""
- date="2020-10-19T18:35:02Z"
- content="""
-Also, /usr/bin/time git-annex find:
-
-       1.70user 0.27system 0:01.55elapsed 126%CPU (0avgtext+0avgdata 97352maxresident)k
-       0inputs+0outputs (0major+9303minor)pagefaults 0swaps
-
-The maxresident seems high, but a stack profile does not show a memory
-leak, or such a large amount of memory use at all. Currently, I
-think that memory is being preallocated by the ghc runtime,
-or something like that. (See [[todo/memory_use_increase]].)
-
-ghc 8.8.4  
-Should keep an eye on this with newer ghc versions.
-"""]]