Don't make a note unless necessary

martinthomson · Dec 20, 2024 · c908911 · c908911
1 parent 64b5ddf
commit c908911
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/setup-note.sh b/setup-note.sh
@@ -50,6 +50,7 @@ if ! wgmeta "$wg"; then
     wg=""
 fi
 
+{
 echo '<note title="Discussion Venues" removeInRFC="true">'
 if [[ -n "$wg" ]]; then
   echo "<t>Discussion of this document takes place on the
@@ -59,3 +60,4 @@ fi
 echo "<t>Source for this draft and an issue tracker can be found at
     <eref target=\"https://${host}/${user}/${repo}\"/>.</t>"
 echo '</note>'
+} > .note.xml
diff --git a/setup.mk b/setup.mk
@@ -93,7 +93,7 @@ README.md: $(LIBDIR)/setup-readme.sh $(drafts_xml) $(filter %.md, $(TEMPLATE_FIL
 
 .PHONY: setup-note
 setup-note: $(LIBDIR)/setup-note.sh
-	$(LIBDIR)/setup-note.sh $(GITHUB_HOST) $(GITHUB_USER) $(GITHUB_REPO) $(drafts_source) >.note.xml
+	$(LIBDIR)/setup-note.sh $(GITHUB_HOST) $(GITHUB_USER) $(GITHUB_REPO) $(drafts_source)
 	if [ -s .note.xml ]; then git add .note.xml; fi
 
 .github/CODEOWNERS: $(LIBDIR)/setup-codeowners.py $(drafts_xml) $(DEPS_FILES)