Menu

#763 Console Font

v1.1.x
closed
v1.1.5
Change Request
2023-02-13
2022-11-24
Bektash
No

Console and History fonts are too small. How do I specify larger fonts?

Analysis:

To provide this feature, we need to first create the corresponding setting for terminal and the history. Then , it is necessary to link the needed updates into the corresponding functions so that changing the font in the options dialog also changes the font in the terminal and the history window.

Implementation:

  • Implementation: Implemented as proposed by the analysis.
  • Revision: [r1294]
  • Implementation test: Font size and font face of editor, history and terminal were changed and changed their appaearing as expected.

Documentation:

  • [x] ChangesLog updated
  • [x] Code changes commented
  • Documentation articles:
    • [ ] corresponding documentation articles updated
    • [ ] new documentation articles created
    • [x] not needed
  • Language files:
    • [x] corresponding language files updated
    • [ ] not needed

Tests:

Tested manually. It is now possible to change the font in the terminal and the history as well as the font size.

Related

Commit: [r1294]

Discussion

  • Erik Hänel

    Erik Hänel - 2022-11-24

    Not yet possible. Thanks for the inquiry. We'll add that to the next release.

     
  • Erik Hänel

    Erik Hänel - 2022-11-24
    • labels: --> gui, terminal, history
    • status: open --> accepted
    • assigned_to: Erik Hänel
    • Version: v1.1.4 --> v1.1.5
     
  • Erik Hänel

    Erik Hänel - 2022-11-25
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -1 +1,23 @@
     Console and History fonts are too small. How do I specify larger fonts? 
    +
    +###Analysis:
    +(*Describe, what's the issue and which changes have to be made*)
    +
    +###Implementation:
    +* Implementation: (*Describe, what you've changed*) 
    +* Revision: [rXXX]
    +* Implementation test: (*Describe the type of test, which you performed, and if it was successful*)
    +
    +###Documentation:
    +* [ ] ChangesLog updated
    +* [ ] Code changes commented
    +* **Documentation articles:**
    
    +    * [ ] corresponding documentation articles updated
    +    * [ ] new documentation articles created
    +    * [ ] not needed
    +* **Language files:**
    +    * [ ] corresponding language files updated
    +    * [ ] not needed
    +
    +###Tests:
    +(*Describe, which tests you performed and their outcome*)
    
    • status: accepted --> analyzing
     
  • Erik Hänel

    Erik Hänel - 2022-12-30
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -1,7 +1,7 @@
     Console and History fonts are too small. How do I specify larger fonts? 
    
     ###Analysis:
    -(*Describe, what's the issue and which changes have to be made*)
    +To provide this feature, we need to first create the corresponding setting for terminal and the history. Then , it is necessary to link the needed updates into the corresponding functions so that changing the font in the options dialog also changes the font in the terminal and the history window.
    
     ###Implementation:
    
     * Implementation: (*Describe, what you've changed*) 
    
    • status: analyzing --> implementing
     
  • Erik Hänel

    Erik Hänel - 2022-12-31
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -4,19 +4,19 @@
     To provide this feature, we need to first create the corresponding setting for terminal and the history. Then , it is necessary to link the needed updates into the corresponding functions so that changing the font in the options dialog also changes the font in the terminal and the history window.
    
     ###Implementation:
    -* Implementation: (*Describe, what you've changed*) 
    -* Revision: [rXXX]
    -* Implementation test: (*Describe the type of test, which you performed, and if it was successful*)
    +* Implementation: Implemented as proposed by the analysis.
    +* Revision: [r1294]
    +* Implementation test: Font size and font face of editor, history and terminal were changed and changed their appaearing as expected.
    
     ###Documentation:
    -* [ ] ChangesLog updated
    -* [ ] Code changes commented
    +* [x] ChangesLog updated
    +* [x] Code changes commented
    
     * **Documentation articles:**
         * [ ] corresponding documentation articles updated
         * [ ] new documentation articles created
    -    * [ ] not needed
    +    * [x] not needed
     * **Language files:**
    -    * [ ] corresponding language files updated
    +    * [x] corresponding language files updated
         * [ ] not needed
    
     ###Tests:
    
    • status: implementing --> testing
     

    Related

    Commit: [r1294]

  • Erik Hänel

    Erik Hänel - 2023-02-13
    • Description has changed:

    Diff:

    --- old
    +++ new
    @@ -20,4 +20,4 @@
    
         * [ ] not needed
    
     ###Tests:
    -(*Describe, which tests you performed and their outcome*)
    +Tested manually. It is now possible to change the font in the terminal and the history as well as the font size.
    
    • status: testing --> closed
     

Anonymous
Anonymous

Add attachments
Cancel





MongoDB Logo MongoDB