From e021597551bce94f8626b1ae24ec746552650170 Mon Sep 17 00:00:00 2001
From: Yihui Xie <xie@yihui.name>
Date: Fri, 7 Aug 2020 13:01:49 -0500
Subject: [PATCH] update option names in the profile file according to
 https://github.com/yihui/tinytex/issues/133#issuecomment-670578215

---
 tools/tinytex.profile | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tools/tinytex.profile b/tools/tinytex.profile
index 27853a1a8..bb9c060d0 100644
--- a/tools/tinytex.profile
+++ b/tools/tinytex.profile
@@ -6,8 +6,8 @@ TEXMFSYSCONFIG ./texmf-config
 TEXMFLOCAL ./texmf-local
 TEXMFSYSVAR ./texmf-var
 
-option_doc 0
-option_src 0
-option_autobackup 0
+tlpdbopt_install_docfiles 0
+tlpdbopt_install_srcfiles 0
+tlpdbopt_autobackup 0
 
-portable 1
+instopt_portable 1