Closed rpkarlin closed 1 year ago
not a "necessary" change but seems like the kind of thing that will cause problems later down the road when the received wisdom dies (i.e., Chris and I, who have already forgotten that comments have to do "# #", leave)
not a "necessary" change but seems like the kind of thing that will cause problems later down the road when the received wisdom dies (i.e., Chris and I, who have already forgotten that comments have to do "# #", leave)