From 558d7b5f624fdaf3b0f5a42ffa4011220885055b Mon Sep 17 00:00:00 2001
From: Benoit Jubin <benoit.jubin@gmail.com>
Date: Sun, 12 Jan 2025 14:40:04 +0100
Subject: [PATCH] Fix a $j-comment.

---
 set.mm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/set.mm b/set.mm
index 9f0754d59..3ef0b4b17 100644
--- a/set.mm
+++ b/set.mm
@@ -93797,7 +93797,7 @@ singletons being the empty set ( ` A e/ _V ` ).  (Contributed by AV,
   1sdom2ALT $p |- 1o ~< 2o $=
     ( c1o csuc c2o csdm com wcel wbr 1onn php4 ax-mp df-2o breqtrri ) AABZCDAEF
     AMDGHAIJKL $.
-  $( $j usage '1sdom2' avoids 'ax-pow'; $)
+  $( $j usage '1sdom2ALT' avoids 'ax-pow'; $)
 
   ${
     $d A x $.  $d A f $.