Added a comment: Another example

diff --git a/doc/todo/git-annex-get_--batch_--key/comment_4_3bd1254c5a24cb3d1c1fd622f2f1e050._comment b/doc/todo/git-annex-get_--batch_--key/comment_4_3bd1254c5a24cb3d1c1fd622f2f1e050._comment
new file mode 100644 (file)
index 0000000..1f27e5c
--- /dev/null
+++ b/doc/todo/git-annex-get_--batch_--key/comment_4_3bd1254c5a24cb3d1c1fd622f2f1e050._comment
@@ -0,0 +1,13 @@
+[[!comment format=mdwn
+ username="https://christian.amsuess.com/chrysn"
+ nickname="chrysn"
+ avatar="http://christian.amsuess.com/avatar/c6c0d57d63ac88f3541522c4b21198c3c7169a665a2f2d733b4f78670322ffdc"
+ subject="Another example"
+ date="2021-08-15T17:42:54Z"
+ content="""
+The program at [[forum/Migrate_mark_files_dead]] shows again how batch-key would be useful, here for `git annex drop --from remote` and `git annex dead`.
+
+I don't have numbers as I can't run it in batch, but comparing to other multi-file batch drop operations, I guesstimate this makes the difference of a script running for an hour invoking git-annex-drop a thousand times (with interruptions if the SSH agent decides to ask confirmation for a key again) or five minutes with --batch-key.
+
+Like with the original use case of annex-to-web, filtering is not an issue for this application.
+"""]]