Documentation Makefile: rename $(O) into $(OPTS)

This patch renames $(O) used in the documentation Makefile
(doc/Makefile) into $(OPTS) in order to avoid a namespace
conflict with $(O) used in the top-level Makefile.

This is in preparation to a new target called 'doc' that will
allow to build the documentation directly from the top-level
Makefile. This is required in order *not* to break setting a
specific build directory, e.g. 'make O=build-test'.

Signed-off-by: Geoffroy Van Cutsem <geoffroy.vancutsem@intel.com>

Author: Geoffroy Van Cutsem

doc/Makefile

@@ -20,7 +20,7 @@ PUBLISHDIR    = ../../projectacrn.github.io/$(RELEASE)
 
 # Put it first so that "make" without argument is like "make help".
 help:
-	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+	@$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(OPTS)
 	@echo ""
 	@echo "make publish"
 	@echo "   publish generated html to projectacrn.github.io site:"
@@ -39,7 +39,7 @@ content:
 	$(Q)scripts/extract_content.py
 
 html: doxy content
-	-$(Q)$(SPHINXBUILD) -t $(DOC_TAG) -b html -d $(BUILDDIR)/doctrees $(SOURCEDIR) $(BUILDDIR)/html $(SPHINXOPTS) $(O) >> doc.log 2>&1
+	-$(Q)$(SPHINXBUILD) -t $(DOC_TAG) -b html -d $(BUILDDIR)/doctrees $(SOURCEDIR) $(BUILDDIR)/html $(SPHINXOPTS) $(OPTS) >> doc.log 2>&1
 	$(Q)./scripts/filter-doc-log.sh doc.log
 
 
@@ -61,6 +61,6 @@ publish:
 
 
 # Catch-all target: route all unknown targets to Sphinx using the new
-# "make mode" option.  $(O) is meant as a shortcut for $(SPHINXOPTS).
+# "make mode" option.  $(OPTS) is meant as a shortcut for $(SPHINXOPTS).
 %: Makefile doxy
-	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O)
+	@$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(OPTS)