(s: string)
| 139 | } |
| 140 | |
| 141 | function decodeEntities(s: string): string { |
| 142 | return s |
| 143 | .replace(/ /g, ' ') |
| 144 | .replace(/&/g, '&') |
| 145 | .replace(/</g, '<') |
| 146 | .replace(/>/g, '>') |
| 147 | .replace(/"/g, '"') |
| 148 | .replace(/'/g, "'"); |
| 149 | } |
| 150 | |
| 151 | /** Store the full clean text so an omitted middle is recoverable via read_file. Best-effort. */ |
| 152 | async function storeFullText(url: string, text: string): Promise<string | null> { |