src/doc/bootstrap: Generate src/doc/en/reference/repl/options.txt

Author: Matthias Koeppe

Makefile

@@ -106,6 +106,7 @@ bootstrap-clean:
 	rm -rf config configure build/make/Makefile-auto.in
 	rm -f src/doc/en/installation/*.txt
 	rm -rf src/doc/en/reference/spkg/*.rst
+	rm -f src/doc/en/reference/repl/*.txt
 
 # Remove absolutely everything which isn't part of the git repo
 maintainer-clean: distclean bootstrap-clean

bootstrap

@@ -160,7 +160,7 @@ save () {
     # Create configure tarball
     echo "Creating $NEWCONFBALL..."
     mkdir -p upstream
-    tar zcf "$NEWCONFBALL" configure config/* build/make/Makefile-auto.in src/doc/en/installation/*.txt src/doc/en/reference/spkg/*.rst
+    tar zcf "$NEWCONFBALL" configure config/* build/make/Makefile-auto.in src/doc/en/installation/*.txt src/doc/en/reference/spkg/*.rst src/doc/en/reference/repl/*.txt
 
     # Update version
     echo "$NEWCONFVERSION" >$PKG/package-version.txt

src/doc/.gitignore

@@ -5,3 +5,4 @@
 /en/reference/spkg/*.rst
 /output
 /en/installation/*.txt
+/en/reference/repl/*.txt

src/doc/bootstrap

@@ -77,3 +77,8 @@ done
 cat >> "$OUTPUT_INDEX" <<EOF
 .. include:: ../footer.txt
 EOF
+
+
+OUTPUT="src/doc/en/reference/repl/options.txt"
+echo >&2 $0:$LINENO: installing "$OUTPUT"
+./sage -advanced > "$OUTPUT"