New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add a command line flag to change the extension of the files generated by the HTML backend #3366

Closed

ice1000 opened this issue Nov 4, 2018 · 2 comments

Assignees

Labels

backend: html command-line type: enhancement

Milestone

Member

ice1000 commented Nov 4, 2018

@vlopezj said in #3313,

I can think of --html-output-extension option, which by default would have the value html, but can be changed to md, or to anything else. An output extension of - could mean outputting to stdout.
For usability, we can also have a --markdown command line flag which would be an alias for the conjunction of flags --html --html-highlight=code --html-output-extension=md. (Another possibility would be for Agda to give sensible default values of --html-highlight and --html-output-extension depending on the extension of the input file(s?); but this seems harder both to document and to implement.).
For even more flexibility, instead of the --html-output-extension option, one can have an --html-output-file option, with which a pattern for filenames can be specified. The default would be --html-output-file=%.html, and the user can give --html-output-file=%.md instead. Output to stdout would be --html-output-file=-, and concatenating all the output to a single file of the user's choosing could be --html-output-file=my-blog-post.md.

I think it'll be a useful feature. Opening an issue so I can refer to when committing.

The text was updated successfully, but these errors were encountered:

ice1000 self-assigned this

ice1000 added command-line backend: html labels

ice1000 added this to the 2.6.0 milestone

Member Author

ice1000 commented Nov 5, 2018

Also, it'll be good to make html-dir, html-highlight, html-output-extension only usable with html flag.

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

0c94d3a

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 mentioned this issue

[ #3366 ] File extension for output of HTML backend #3367

Merged

vlopezj mentioned this issue

Release Agda 2.5.4.3 #3369

Closed

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

04fff3a

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

a40c91d

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Refactor file type detection, add iFileType field for…

8da135c

… `Interface`

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Fix typo

2f5935d

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation for agda#3366

fd380f7

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

0f45fe9

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Refactor file type detection, add iFileType field for…

c8f3bea

… `Interface`

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Fix typo

552ceeb

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation for agda#3366

ddd3d8b

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

65545b1

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Refactor file type detection, add iFileType field for…

df30264

… `Interface`

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Fix typo

f1142c0

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

19fc1b1

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation and changelog for agda#3366

d97995f

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation and changelog for agda#3366

b668165

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

b724d37

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Refactor file type detection, add iFileType field for…

62f41f2

… `Interface`

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Fix typo

60bd78e

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

07da559

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation and changelog for agda#3366

d4827ff

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

8c1c7ec

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

8fbf085

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Added initial support, will document later

a9bad1b

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Refactor file type detection, add iFileType field for…

c285779

… `Interface`

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Fix typo

b0372dc

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

6c5bcd9

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ doc ] Documentation and changelog for agda#3366

cf86696

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Address comments

1ef929f

Signed-off-by: ice1000 <ice1000kotlin@foxmail.com>

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Minor fixes, changelogs and documentations

ice1000 added a commit to Agda-zh/agda that referenced this issue


          [ agda#3366 ] Add tests

30dcb47

ice1000 added a commit that referenced this issue


          Merge pull request #3367 from Agda-zh/custom-ext-html

a9b9a3b

[ #3366 ]  File extension for output of HTML backend

Member Author

ice1000 commented Nov 12, 2018

Closed by #3367

ice1000 closed this as completed

asr added the type: enhancement label

ice1000 mentioned this issue

Generate a Jekyll-compatible website with HTML backend #3386

Closed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment