Makefile: fix a comment

diff --git a/Makefile b/Makefile
index a213c0713bb357059e335636305be15406e002a3..1674606b61600ca772f9bc66368393e8af237640 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,7 @@ workspace: $(WORKSPACEFILES)
 workspace/src/%.rs: src/%.rs Makefile dup-unimpl.sed
        @mkdir -p .tmp/docs
        @echo "$< -> $@"
-       @# sed-fu: remove lines starting with "//@", and replace those ending in "/*@*/" by "unimplemented!()".
+       @# sed-fu: remove lines starting with "//@", and replace those ending in "/*@*/" or "/*@@*/" by "unimplemented!()".
        @# Also coalesce multiple adjacent such lines to one.
        @sed '/^\s*\/\/@/d;s|\(\s*\)\S.*/\*@@\?\*/|\1unimplemented!()|' $< | sed -f dup-unimpl.sed > $@